CPP 2021 – Proceedings

10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021)

Frontmatter

Invited Talks

Teaching Algorithms and Data Structures with a Proof Assistant (Invited Talk)
Tobias Nipkow
(TU Munich, Germany)


@InProceedings{CPP21p1, author = {Tobias Nipkow}, title = {Teaching Algorithms and Data Structures with a Proof Assistant (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3437992.3439910}, year = {2021}, } Publisher's Version

Underpinning the Foundations: Sail-Based Semantics, Testing, and Reasoning for Production and CHERI-Enabled Architectures (Invited Talk)
Peter Sewell
(University of Cambridge, UK)


@InProceedings{CPP21p22, author = {Peter Sewell}, title = {Underpinning the Foundations: Sail-Based Semantics, Testing, and Reasoning for Production and CHERI-Enabled Architectures (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {22-21}, doi = {10.1145/3437992.3439911}, year = {2021}, } Publisher's Version

AI and Machine Learning

A Formal Proof of PAC Learnability for Decision Stumps
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan
(Boston College, USA; University of Pittsburgh, USA; IMDEA Software Institute, Spain)


@InProceedings{CPP21p43, author = {Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Jean-Baptiste Tristan}, title = {A Formal Proof of PAC Learnability for Decision Stumps}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {43-42}, doi = {10.1145/3437992.3439917}, year = {2021}, } Publisher's Version

CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton
(University of Pittsburgh, USA; IBM Research, USA; IHES, France)


@InProceedings{CPP21p64, author = {Koundinya Vajjha and Avraham Shinnar and Barry Trager and Vasily Pestun and Nathan Fulton}, title = {CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {64-63}, doi = {10.1145/3437992.3439927}, year = {2021}, } Publisher's Version

Compilers and Interpreters

A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)
Magnus O. Myreen
(Chalmers University of Technology, Sweden)


@InProceedings{CPP21p85, author = {Magnus O. Myreen}, title = {A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {85-84}, doi = {10.1145/3437992.3439915}, year = {2021}, } Publisher's Version

Lutsig: A Verified Verilog Compiler for Verified Circuit Development
Andreas Lööw
(Chalmers University of Technology, Sweden)


@InProceedings{CPP21p106, author = {Andreas Lööw}, title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {106-105}, doi = {10.1145/3437992.3439916}, year = {2021}, } Publisher's Version

Towards Efficient and Verified Virtual Machines for Dynamic Languages
Martin Desharnais and Stefan Brunthaler
(Bundeswehr University Munich, Germany)


@InProceedings{CPP21p127, author = {Martin Desharnais and Stefan Brunthaler}, title = {Towards Efficient and Verified Virtual Machines for Dynamic Languages}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {127-126}, doi = {10.1145/3437992.3439923}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

Program Logics

Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Simon Friis Vindum and Lars Birkedal
(Aarhus University, Denmark)


@InProceedings{CPP21p148, author = {Simon Friis Vindum and Lars Birkedal}, title = {Contextual Refinement of the Michael-Scott Queue (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {148-147}, doi = {10.1145/3437992.3439930}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

Reasoning about Monotonicity in Separation Logic
Amin Timany and Lars Birkedal
(Aarhus University, Denmark)


@InProceedings{CPP21p169, author = {Amin Timany and Lars Birkedal}, title = {Reasoning about Monotonicity in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {169-168}, doi = {10.1145/3437992.3439931}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

Security, Blockchains, and Smart Contracts

Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)


@InProceedings{CPP21p190, author = {Danil Annenkov and Mikkel Milo and Jakob Botsch Nielsen and Bas Spitters}, title = {Extracting Smart Contracts Tested and Verified in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {190-189}, doi = {10.1145/3437992.3439934}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr.
(Dfinity Foundation, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; INESC TEC, Portugal)


@InProceedings{CPP21p211, author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.}, title = {Formal Verification of Authenticated, Append-Only Skip Lists in Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {211-210}, doi = {10.1145/3437992.3439924}, year = {2021}, } Publisher's Version

Towards Formally Verified Compilation of Tag-Based Policy Enforcement
CHR Chhak, Andrew Tolmach, and Sean Anderson
(Portland State University, USA)


@InProceedings{CPP21p232, author = {CHR Chhak and Andrew Tolmach and Sean Anderson}, title = {Towards Formally Verified Compilation of Tag-Based Policy Enforcement}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {232-231}, doi = {10.1145/3437992.3439929}, year = {2021}, } Publisher's Version

Semantics

A Coq Formalization of Data Provenance
Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, and Rébecca Zucchini
(LRI, France; University of Paris-Saclay, France; CNRS, France)


@InProceedings{CPP21p253, author = {Véronique Benzaken and Sarah Cohen-Boulakia and Évelyne Contejean and Chantal Keller and Rébecca Zucchini}, title = {A Coq Formalization of Data Provenance}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {253-252}, doi = {10.1145/3437992.3439920}, year = {2021}, } Publisher's Version

Developing and Certifying Datalog Optimizations in Coq/MathComp
Pierre-Léo Bégay, Pierre Crégut, and Jean-François Monin
(Orange Labs, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France)


@InProceedings{CPP21p274, author = {Pierre-Léo Bégay and Pierre Crégut and Jean-François Monin}, title = {Developing and Certifying Datalog Optimizations in Coq/MathComp}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {274-273}, doi = {10.1145/3437992.3439913}, year = {2021}, } Publisher's Version

Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson
(IT University of Copenhagen, Denmark; University of Amsterdam, Netherlands; Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)


@InProceedings{CPP21p295, author = {Jonas Kastberg Hinrichsen and Daniël Louwrink and Robbert Krebbers and Jesper Bengtson}, title = {Machine-Checked Semantic Session Typing}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {295-294}, doi = {10.1145/3437992.3439914}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

Proof Tactics

A Novice-Friendly Induction Tactic for Lean
Jannis Limperg
(Vrije Universiteit Amsterdam, Netherlands)


@InProceedings{CPP21p316, author = {Jannis Limperg}, title = {A Novice-Friendly Induction Tactic for Lean}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {316-315}, doi = {10.1145/3437992.3439928}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar
(MPI-SWS, Germany; McGill University, Canada)


@InProceedings{CPP21p337, author = {Heiko Becker and Nathaniel Bos and Ivan Gavran and Eva Darulova and Rupak Majumdar}, title = {Lassie: HOL4 Tactics by Example}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {337-336}, doi = {10.1145/3437992.3439925}, year = {2021}, } Publisher's Version

Rewriting and Automated Reasoning

A Modular Isabelle Framework for Verifying Saturation Provers
Sophie Tourret and Jasmin Blanchette
(MPI-INF, Germany; Vrije Universiteit Amsterdam, Netherlands)


@InProceedings{CPP21p358, author = {Sophie Tourret and Jasmin Blanchette}, title = {A Modular Isabelle Framework for Verifying Saturation Provers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {358-357}, doi = {10.1145/3437992.3439912}, year = {2021}, } Publisher's Version

An Isabelle/HOL Formalization of AProVE’s Termination Method for LLVM IR
Max W. Haslbeck and René Thiemann
(University of Innsbruck, Austria)


@InProceedings{CPP21p379, author = {Max W. Haslbeck and René Thiemann}, title = {An Isabelle/HOL Formalization of AProVE’s Termination Method for LLVM IR}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {379-378}, doi = {10.1145/3437992.3439935}, year = {2021}, } Publisher's Version

A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, and Bertram Felgenhauer
(University of Innsbruck, Austria)


@InProceedings{CPP21p400, author = {Alexander Lochmann and Aart Middeldorp and Fabian Mitterwallner and Bertram Felgenhauer}, title = {A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {400-399}, doi = {10.1145/3437992.3439918}, year = {2021}, } Publisher's Version

Formalized Mathematics

Formalizing the Ring of Witt Vectors
Johan Commelin and Robert Y. Lewis
(University of Freiburg, Germany; Vrije Universiteit Amsterdam, Netherlands)


@InProceedings{CPP21p421, author = {Johan Commelin and Robert Y. Lewis}, title = {Formalizing the Ring of Witt Vectors}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {421-420}, doi = {10.1145/3437992.3439919}, year = {2021}, } Publisher's Version

Formal Verification of Semi-algebraic Sets and Real Analytic Functions
J. Tanner Slagel, Lauren White, and Aaron Dutle
(NASA Langley Research Center, USA; Kansas State University, USA)


@InProceedings{CPP21p442, author = {J. Tanner Slagel and Lauren White and Aaron Dutle}, title = {Formal Verification of Semi-algebraic Sets and Real Analytic Functions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {442-441}, doi = {10.1145/3437992.3439933}, year = {2021}, } Publisher's Version

On the Formalisation of Kolmogorov Complexity
Elliot Catt and Michael Norrish
(Australian National University, Australia; Data61 at CSIRO, Australia)


@InProceedings{CPP21p463, author = {Elliot Catt and Michael Norrish}, title = {On the Formalisation of Kolmogorov Complexity}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {463-462}, doi = {10.1145/3437992.3439921}, year = {2021}, } Publisher's Version

Logic, Set Theory, and Category Theory

An Anti-Locally-Nameless Approach to Formalizing Quantifiers
Olivier Laurent
(CNRS, France; ENS Lyon, France)


@InProceedings{CPP21p484, author = {Olivier Laurent}, title = {An Anti-Locally-Nameless Approach to Formalizing Quantifiers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {484-483}, doi = {10.1145/3437992.3439926}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Dominik Kirst and Felix Rech
(Saarland University, Germany)


@InProceedings{CPP21p505, author = {Dominik Kirst and Felix Rech}, title = {The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {505-504}, doi = {10.1145/3437992.3439932}, year = {2021}, } Publisher's Version

Formalizing Category Theory in Agda
Jason Z. S. Hu and Jacques Carette
(McGill University, Canada; McMaster University, Canada)


@InProceedings{CPP21p526, author = {Jason Z. S. Hu and Jacques Carette}, title = {Formalizing Category Theory in Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {526-525}, doi = {10.1145/3437992.3439922}, year = {2021}, } Publisher's Version Published Artifact Artifacts Available

proc time: 0.78