CPP 2022 – Proceedings

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

Frontmatter

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)

Publisher's Version Article: poplws22cppmain-key4-p doi:10.1145/3497775.3505265

Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk)
Andrew W. Appel
(Princeton University, USA)

Publisher's Version Article: poplws22cppmain-key2-p doi:10.1145/3497775.3503951

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

Publisher's Version Article: poplws22cppmain-key3-p doi:10.1145/3497775.3503949

Program Verification

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

Publisher's Version Article: poplws22cppmain-p28-p doi:10.1145/3497775.3503686

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

Publisher's Version Article: poplws22cppmain-p57-p doi:10.1145/3497775.3503694

Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; Verimag, France; ENS Lyon, France)

Publisher's Version Article: poplws22cppmain-p16-p doi:10.1145/3497775.3503679

Semantics

Certified Abstract Machines for Skeletal Semantics
Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt
(University of Rennes, France; University of Lorraine, France; Inria, France)

Publisher's Version Article: poplws22cppmain-p8-p doi:10.1145/3497775.3503676

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)

Publisher's Version Article: poplws22cppmain-p24-p doi:10.1145/3497775.3503685

Verified Data Structures

Specification and Verification of a Transient Stack
Alexandre Moine, Arthur Charguéraud, and François Pottier
(Inria, France; University of Strasbourg, France; CNRS, France)

Publisher's Version Article: poplws22cppmain-p9-p doi:10.1145/3497775.3503677

Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
Simon Friis Vindum, Dan Frumin, and Lars Birkedal
(Aarhus University, Denmark; University of Groningen, Netherlands)

Publisher's Version Article: poplws22cppmain-p37-p doi:10.1145/3497775.3503689

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

Publisher's Version Article: poplws22cppmain-p18-p doi:10.1145/3497775.3503681

Distributed Systems and Concurrency

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

Publisher's Version Article: poplws22cppmain-p29-p doi:10.1145/3497775.3503687

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

Publisher's Version Article: poplws22cppmain-p30-p doi:10.1145/3497775.3503688

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, Israel)

Publisher's Version Article: poplws22cppmain-p7-p doi:10.1145/3497775.3503675

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

Publisher's Version Article: poplws22cppmain-p47-p doi:10.1145/3497775.3503693

Proof Infrastructure

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

Publisher's Version Article: poplws22cppmain-p6-p doi:10.1145/3497775.3503674

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

Publisher's Version Article: poplws22cppmain-p45-p doi:10.1145/3497775.3503692

Rewriting and Automated Reasoning

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

Publisher's Version Article: poplws22cppmain-p42-p doi:10.1145/3497775.3503691

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

Publisher's Version Article: poplws22cppmain-p22-p doi:10.1145/3497775.3503683

Formalized Mathematics

Formalising Lie Algebras
Oliver Nash
(Imperial College London, UK)

Publisher's Version Article: poplws22cppmain-p3-p doi:10.1145/3497775.3503672

Windmills of the Minds: An Algorithm for Fermat’s Two Squares Theorem
Hing Lun Chan
(Australian National University, Australia)

Publisher's Version Article: poplws22cppmain-p4-p doi:10.1145/3497775.3503673

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

Publisher's Version Article: poplws22cppmain-p20-p doi:10.1145/3497775.3503682

Formalization of Logic

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

Publisher's Version Article: poplws22cppmain-p23-p doi:10.1145/3497775.3503684

Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
Dan Frumin
(University of Groningen, Netherlands)

Publisher's Version Article: poplws22cppmain-p38-p doi:10.1145/3497775.3503690

Category Theory and HoTT

Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg
(TU Delft, Netherlands; University of Birmingham, UK; IRIT, France; Université de Toulouse, France; CNRS, France; Toulouse INP, France; UT3, France; Stockholm University, Sweden)

Publisher's Version Article: poplws22cppmain-p10-p doi:10.1145/3497775.3503678

(Deep) Induction Rules for GADTs
Patricia Johann and Enrico Ghiorzi
(Appalachian State University, USA)

Publisher's Version Article: poplws22cppmain-p17-p doi:10.1145/3497775.3503680

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

Publisher's Version Article: poplws22cppmain-p1-p doi:10.1145/3497775.3503671

proc time: 0.04