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)


@InProceedings{CPP22p1, author = {June Andronick}, title = {The seL4 Verification: The Art and Craft of Proof and the Reality of Commercial Support (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3497775.3505265}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p24, author = {Andrew W. Appel}, title = {Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {24-23}, doi = {10.1145/3497775.3503951}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p47, author = {César Muñoz}, title = {Structural Embeddings Revisited (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {47-46}, doi = {10.1145/3497775.3503949}, year = {2022}, } 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)


@InProceedings{CPP22p70, author = {Louis Cheung and Liam O'Connor and Christine Rizkallah}, title = {Overcoming Restraint: Composing Verification of Foreign Functions with Cogent}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {70-69}, doi = {10.1145/3497775.3503686}, year = {2022}, } 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)


@InProceedings{CPP22p93, author = {Derek Egolf and Sam Lasser and Kathleen Fisher}, title = {Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {93-92}, doi = {10.1145/3497775.3503694}, year = {2022}, } 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)


@InProceedings{CPP22p116, author = {Cyril Six and Léo Gourdin and Sylvain Boulmé and David Monniaux and Justus Fasse and Nicolas Nardino}, title = {Formally Verified Superblock Scheduling}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {116-115}, doi = {10.1145/3497775.3503679}, year = {2022}, } Publisher's Version

Semantics

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


@InProceedings{CPP22p139, author = {Guillaume Ambal and Sergueï Lenglet and Alan Schmitt}, title = {Certified Abstract Machines for Skeletal Semantics}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {139-138}, doi = {10.1145/3497775.3503676}, year = {2022}, } 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)


@InProceedings{CPP22p162, author = {Esther Conrad and Laura Titolo and Dimitra Giannakopoulou and Thomas Pressburger and Aaron Dutle}, title = {A Compositional Proof Framework for FRETish Requirements}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {162-161}, doi = {10.1145/3497775.3503685}, year = {2022}, } 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)


@InProceedings{CPP22p185, author = {Alexandre Moine and Arthur Charguéraud and François Pottier}, title = {Specification and Verification of a Transient Stack}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {185-184}, doi = {10.1145/3497775.3503677}, year = {2022}, } 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)


@InProceedings{CPP22p208, author = {Simon Friis Vindum and Dan Frumin and Lars Birkedal}, title = {Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {208-207}, doi = {10.1145/3497775.3503689}, year = {2022}, } 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)


@InProceedings{CPP22p231, author = {Quentin Carbonneaux and Noam Zilberstein and Christoph Klee and Peter W. O'Hearn and Francesco Zappa Nardelli}, title = {Applying Formal Verification to Microkernel IPC at Meta}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {231-230}, doi = {10.1145/3497775.3503681}, year = {2022}, } Publisher's Version

Distributed Systems and Concurrency

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


@InProceedings{CPP22p254, author = {Sarah Spall and Neil Mitchell and Sam Tobin-Hochstadt}, title = {Forward Build Systems, Formally}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {254-253}, doi = {10.1145/3497775.3503687}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p277, author = {William Schultz and Ian Dardik and Stavros Tripakis}, title = {Formal Verification of a Distributed Dynamic Reconfiguration Protocol}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {277-276}, doi = {10.1145/3497775.3503688}, year = {2022}, } 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)


@InProceedings{CPP22p300, author = {Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman}, title = {A Verified Algebraic Representation of Cairo Program Execution}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {300-299}, doi = {10.1145/3497775.3503675}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p323, author = {Denis Firsov and Dominique Unruh}, title = {Reflection, Rewinding, and Coin-Toss in EasyCrypt}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {323-322}, doi = {10.1145/3497775.3503693}, year = {2022}, } Publisher's Version

Proof Infrastructure

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


@InProceedings{CPP22p346, author = {Mihails Milehins}, title = {An Extension of the Framework Types-To-Sets for Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {346-345}, doi = {10.1145/3497775.3503674}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p369, author = {Pablo Donato and Pierre-Yves Strub and Benjamin Werner}, title = {A Drag-and-Drop Proof Tactic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {369-368}, doi = {10.1145/3497775.3503692}, year = {2022}, } 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)


@InProceedings{CPP22p392, author = {Shuanglong Kan and Anthony Widjaja Lin and Philipp Rümmer and Micha Schrader}, title = {CertiStr: A Certified String Solver}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {392-391}, doi = {10.1145/3497775.3503691}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p415, author = {Michael Färber}, title = {Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {415-414}, doi = {10.1145/3497775.3503683}, year = {2022}, } Publisher's Version

Formalized Mathematics

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


@InProceedings{CPP22p438, author = {Oliver Nash}, title = {Formalising Lie Algebras}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {438-437}, doi = {10.1145/3497775.3503672}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p461, author = {Hing Lun Chan}, title = {Windmills of the Minds: An Algorithm for Fermat’s Two Squares Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {461-460}, doi = {10.1145/3497775.3503673}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p484, author = {Ariel Kellison}, title = {A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {484-483}, doi = {10.1145/3497775.3503682}, year = {2022}, } Publisher's Version

Formalization of Logic

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


@InProceedings{CPP22p507, author = {Mark Koch and Dominik Kirst}, title = {Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {507-506}, doi = {10.1145/3497775.3503684}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p530, author = {Dan Frumin}, title = {Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {530-529}, doi = {10.1145/3497775.3503690}, year = {2022}, } 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)


@InProceedings{CPP22p553, author = {Benedikt Ahrens and Ralph Matthes and Anders Mörtberg}, title = {Implementing a Category-Theoretic Framework for Typed Abstract Syntax}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {553-552}, doi = {10.1145/3497775.3503678}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p576, author = {Patricia Johann and Enrico Ghiorzi}, title = {(Deep) Induction Rules for GADTs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {576-575}, doi = {10.1145/3497775.3503680}, year = {2022}, } Publisher's Version

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


@InProceedings{CPP22p599, author = {Jonathan Prieto-Cubides}, title = {On Homotopy of Walks and Spherical Maps in Homotopy Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {599-598}, doi = {10.1145/3497775.3503671}, year = {2022}, } Publisher's Version

proc time: 0.75