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)

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)

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)

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)

Publisher's Version Info

Compilers and Interpreters

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

Publisher's Version

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

Publisher's Version

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

Publisher's Version

Program Logics

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

Publisher's Version

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

Publisher's Version

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)

Publisher's Version Info

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)

Publisher's Version

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

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)

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)

Publisher's Version Info

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)

Publisher's Version

Proof Tactics

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

Publisher's Version

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

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)

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)

Publisher's Version Info

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)

Publisher's Version Info

Formalized Mathematics

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

Publisher's Version Info

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)

Publisher's Version

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

Publisher's Version

Logic, Set Theory, and Category Theory

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

Publisher's Version

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

Publisher's Version Info

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

Publisher's Version

proc time: 5.23