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)


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)
Article Search
Structural Embeddings Revisited (Invited Talk)
César Muñoz
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


Certified Abstract Machines for Skeletal Semantics
Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt
(University of Rennes, France; University of Lorraine, France; Inria, France)
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)
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)
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)
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)
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)
Article Search
On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
Jonathan Prieto-Cubides
(University of Bergen, Norway)
Article Search

proc time: 1.69