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

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 Article Search
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 Search
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain BoulméORCID logo, David MonniauxORCID logo, 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 Search 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 Article Search
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 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; University of Strasbourg, France; CNRS, France)
Publisher's Version Article Search
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 Article Search
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, 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 Article Search

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 Search
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, and Stavros Tripakis
(Northeastern University, USA)
Publisher's Version Article Search

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

Proof Infrastructure

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

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

Formalized Mathematics

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

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 Article Search Info
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
Dan FruminORCID logo
(University of Groningen, Netherlands)
Publisher's Version 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; Université de Toulouse, France; CNRS, France; Toulouse INP, France; UT3, France; Stockholm University, Sweden)
Publisher's Version Article Search
(Deep) Induction Rules for GADTs
Patricia Johann and Enrico Ghiorzi ORCID logo
(Appalachian State University, USA)
Publisher's Version Article Search
On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
Jonathan Prieto-Cubides
(University of Bergen, Norway)
Publisher's Version Article Search Info

proc time: 4.9