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 – Proceedings

Contents - Abstracts - Authors

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

Frontmatter

Title Page
Welcome from the Chairs
CPP 2022 Organization Team
CPP 2022 Financial Supporters

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
Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk)
Andrew W. Appel
(Princeton University, USA)
Publisher's Version
Structural Embeddings Revisited (Invited Talk)
César Muñoz
(AWS, USA)
Publisher's Version

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
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
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 Info

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
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

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
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
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

Distributed Systems and Concurrency

Forward Build Systems, Formally
Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt
(Indiana University, USA; Meta, UK)
Publisher's Version
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, and Stavros Tripakis
(Northeastern University, USA)
Publisher's Version

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 Info
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

Proof Infrastructure

An Extension of the Framework Types-To-Sets for Isabelle/HOL
Mihails Milehins
Publisher's Version
A Drag-and-Drop Proof Tactic
Pablo Donato, Pierre-Yves Strub, and Benjamin Werner
(École Polytechnique, France)
Publisher's Version

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
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
Michael Färber
(University of Innsbruck, Austria)
Publisher's Version

Formalized Mathematics

Formalising Lie Algebras
Oliver Nash
(Imperial College London, UK)
Publisher's Version
Windmills of the Minds: An Algorithm for Fermat’s Two Squares Theorem
Hing Lun Chan
(Australian National University, Australia)
Publisher's Version
A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
Ariel Kellison
(Cornell University, USA)
Publisher's Version

Formalization of Logic

Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
Mark Koch and Dominik Kirst
(Saarland University, Germany)
Publisher's Version Info
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
Dan Frumin
(University of Groningen, Netherlands)
Publisher's Version

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
(Deep) Induction Rules for GADTs
Patricia Johann and Enrico Ghiorzi
(Appalachian State University, USA)
Publisher's Version
On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
Jonathan Prieto-Cubides
(University of Bergen, Norway)
Publisher's Version Info

proc time: 3.09