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. AppelORCID logo
(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 ORCID logo, Liam O'ConnorORCID logo, and Christine Rizkallah ORCID logo
(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 ORCID logo, Sylvain BoulméORCID logo, David MonniauxORCID logo, Justus Fasse ORCID logo, 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 ORCID logo, Laura TitoloORCID logo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle ORCID logo
(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 ORCID logo, Arthur CharguéraudORCID logo, and François PottierORCID logo
(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 VindumORCID logo, Dan Frumin ORCID logo, and Lars BirkedalORCID logo
(Aarhus University, Denmark; University of Groningen, Netherlands)
Publisher's Version
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein ORCID logo, Christoph Klee, Peter W. O'Hearn ORCID logo, 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 AvigadORCID logo, 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 ORCID logo and Dominique Unruh ORCID logo
(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 ORCID logo, 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ärberORCID logo
(University of Innsbruck, Austria)
Publisher's Version

Formalized Mathematics

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

Formalization of Logic

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

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; 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 ORCID logo
(Appalachian State University, USA)
Publisher's Version
On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
Jonathan Prieto-Cubides ORCID logo
(University of Bergen, Norway)
Publisher's Version Info

proc time: 6.08