POPL 2022 Co-Located Events
POPL 2022 Co-Located Events
Powered by
Conference Publishing Consulting

11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), January 17-18, 2022, Philadelphia, PA, USA

CPP 2022 – Preliminary Table of Contents

Contents - Abstracts - Authors

11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022)

Frontmatter

Title Page


Message from the Chairs


Invited Talks

The seL4 Verification: The Art and Craft of Proof and the Reality of Commercial Support (Invited Talk)
June Andronick
(Proofcraft, Australia; UNSW, Australia; seL4 Foundation, Australia)


Article Search
Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk)
Andrew W. AppelORCID logo
(Princeton University, USA)
Program verification in the large is not only a matter of mechanizing a program logic to handle the semantics of your programming language. You must reason in the mathematics of your application domain--and there are many application domains, each with their own community of domain experts. So you will need to import mechanized proof theories from many domains, and they must all interoperate. Such an ecosystem is not only a matter of mathematics, it is a matter of software process engineering and social engineering. Coq's ecosystem has been maturing nicely in these senses.

Article Search
Structural Embeddings Revisited (Invited Talk)
César Muñoz
(AWS, USA; NASA, USA)


Article Search

Program Verification

Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Louis Cheung ORCID logo, Liam O'Connor, and Christine Rizkallah
(UNSW, Australia; University of Edinburgh, UK)


Article Search
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Derek Egolf, Sam Lasser, and Kathleen Fisher
(Northeastern University, USA; Tufts University, USA)


Article Search
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain BoulméORCID logo, David MonniauxORCID logo, Justus Fasse, and Nicolas Nardino
(Kalray, n.n.; Grenoble Alps University, France; CNRS, France; ENS Lyon, France)


Article Search

Semantics

Certified Abstract Machines for Skeletal Semantics
Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt
(University of Rennes, France; University of Lorraine, France; Inria, France)
Skeletal semantics is a framework to describe semantics of programming languages. We propose an automatic generation of a certified OCaml interpreter for any language written in skeletal semantics. To this end, we introduce two new interpretations, i.e., formal meanings, of skeletal semantics, in the form of non-deterministic and deterministic abstract machines. These machines are derived from the usual big-step interpretation of skeletal semantics using functional correspondence, a standard transformation from big-step evaluators to abstract machines. All these interpretations are formalized in the Coq proof assistant and we certify their soundness. We finally use the extraction from Coq to OCaml to obtain the certified interpreter.

Article Search
A Compositional Proof Framework for FRETish Requirements
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle
(NASA Langley Research Center, USA; National Institute of Aerospace, USA; NASA Ames Research Center, USA)


Article Search

Verified Data Structures

Specification and Verification of a Transient Stack
Alexandre Moine ORCID logo, Arthur Charguéraud, and François PottierORCID logo
(Inria, France)
A transient data structure is a package of an ephemeral data structure, a persistent data structure, and fast conversions between them. In this paper, we describe the specification and proof of a transient stack and its iterators. This data structure is a scaled-down version of the general-purpose transient sequence data structure implemented in the OCaml library Sek. Internally, it relies on fixed-capacity arrays, or chunks, which can be shared between several ephemeral and persistent stacks. Dynamic tests are used to determine whether a chunk can be updated in place or must be copied: a chunk can be updated if it is uniquely owned or if the update is monotonic. Using CFML, which implements Separation Logic with Time Credits inside Coq, we verify the functional correctness and the amortized time complexity of this data structure and of its iterators. The specification of iterators describes what the operations on iterators do, how much they cost, and under what circumstances an iterator is invalidated.

Article Search
Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook’s Folly Library
Simon Friis Vindum ORCID logo, Lars BirkedalORCID logo, and Dan Frumin
(Aarhus University, Denmark; University of Groningen, Netherlands)
We present the first formal specification and verification of the fine-grained concurrent multi-producer-multi-consumer queue algorithm from Meta’s C++ library Folly of core infrastructure components. The queue is highly optimized, practical, and used by Meta in production where it scales to thousands of consumer and producer threads. We present an implementation of the algorithm in an ML-like language and formally prove that it is a contextual refinement of a simple coarse-grained queue (a property that implies that the MPMC queue is linearizable). We use the ReLoC relational logic and the Iris program logic to carry out the proof and to mechanize it in the Coq proof assistant. The MPMC queue is implemented using three modules, and our proof is similarly modular. By using ReLoC and Iris’s support for modular reasoning we verify each module in isolation and compose these together. A key challenge of the MPMC queue is that it has a so-called external linearization point, which ReLoC has no support for reasoning about. Thus we extend ReLoC, both on paper and in Coq, with novel support for reasoning about external linearization points.

Article Search
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, and Francesco Zappa Nardelli
(Facebook, France; Facebook, USA; Cornell University, USA; Facebook, n.n.; Facebook, UK; University College London, UK)


Article Search

Distributed Systems and Concurrency

Forward Build Systems, Formally
Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt
(Indiana University, USA; Facebook, UK)


Article Search
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, and Stavros Tripakis
(Northeastern University, USA)


Article Search

Blockchains and Cryptography

A Verified Algebraic Representation of Cairo Program Execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman
(Carnegie Mellon University, USA; Starkware Industries, n.n.)


Article Search
Reflection, Rewinding, and Coin-Toss in EasyCrypt
Denis Firsov ORCID logo and Dominique Unruh ORCID logo
(Tallinn University of Technology, Estonia; University of Tartu, Estonia)


Article Search

Proof Infrastructure

An Extension of the Framework Types-To-Sets for Isabelle/HOL
Mihails Milehins


Article Search
A Drag-and-Drop Proof Tactic
Benjamin Werner, Pablo Donato ORCID logo, and Pierre-Yves Strub
(École Polytechnique, France)


Article Search

Rewriting and Automated Reasoning

CertiStr: A Certified String Solver
Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer ORCID logo, and Micha Schrader
(TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)


Article Search
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
Michael FärberORCID logo
(University of Innsbruck, Austria)


Article Search

Formalized Mathematics

Formalising Lie Algebras
Oliver NashORCID logo
(Imperial College London, UK)


Article Search
Windmills of the Minds: An Algorithm for Fermat’s Two Squares Theorem
Hing Lun Chan ORCID logo
(Australian National University, Australia)
The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence ''proof from the Book''. Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a finite set, especially the parity of the number of fixed points in the involutions. Starting as an existence proof that is non-constructive, there is an ingenious way to turn it into a constructive one. This gives an algorithm to compute the two squares by iterating the two involutions alternatively from a known fixed point.

Article Search
A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
Ariel Kellison
(Cornell University, USA)


Article Search

Formalization of Logic

Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
Mark Koch and Dominik Kirst
(Saarland University, Germany)


Article Search
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
Dan Frumin
(University of Groningen, Netherlands)
The logic of bunched implications (BI) is a substructural logic that forms the backbone of separation logic, the much studied logic for reasoning about heap-manipulating programs. Although the proof theory and metatheory of BI are mathematically involved, the formalization of important metatheoretical results is still incipient. In this paper we present a self-contained formalized, in the Coq proof assistant, proof of a central metatheoretical property of BI: cut elimination for its sequent calculus.
The presented proof is semantic, in the sense that is obtained by interpreting sequents in a particular “universal” model. This results in a more modular and elegant proof than a standard Gentzen-style cut elimination argument, which can be subtle and error-prone in manual proofs for BI. In particular, our semantic approach avoids unnecessary inversions on proof derivations, or the uses of cut reductions and the multi-cut rule.
Besides modular, our approach is also robust: we demonstrate how our method scales, with minor modifications, to (i) an extension of BI with an arbitrary set of simple structural rules, and (ii) an extension with an S4-like □ modality.

Article Search

Category Theory and HoTT

Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt AhrensORCID logo, Ralph MatthesORCID logo, and Anders MörtbergORCID logo
(TU Delft, Netherlands; University of Birmingham, UK; IRIT, France; University of Toulouse, France; CNRS, France; Toulouse INP, France; UT3, France; Stockholm University, Sweden)


Article Search
(Deep) Induction Rules for GADTs
Patricia Johann and Enrico Ghiorzi ORCID logo
(Appalachian State University, USA)
Deep data types are those that are constructed from other data types, including, possibly, themselves. In this case, they are said to be truly nested. Deep induction is an extension of structural induction that traverses all of the structure in a deep data type, propagating predicates on its primitive data throughout the entire structure. Deep induction can be used to prove properties of nested types, including truly nested types, that cannot be proved via structural induction. In this paper we show how to extend deep induction to GADTs that are not truly nested GADTs. This opens the way to incorporating automatic generation of (deep) induction rules for them into proof assistants. We also show that the techniques developed in this paper do not suffice for extending deep induction to truly nested GADTs, so more sophisticated techniques are needed to derive deep induction rules for them.

Article Search
On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
Jonathan Prieto-Cubides
(University of Bergen, Norway)


Article Search

proc time: 2.7