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 Article: poplws21cppmain-inv2-p doi:10.1145/3437992.3439910

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 Article: poplws21cppmain-inv1-p doi:10.1145/3437992.3439911

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 Article: poplws21cppmain-p15-p doi:10.1145/3437992.3439917

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 Article: poplws21cppmain-p30-p doi:10.1145/3437992.3439927

Compilers and Interpreters

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

Publisher's Version Article: poplws21cppmain-p10-p doi:10.1145/3437992.3439915

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

Publisher's Version Article: poplws21cppmain-p11-p doi:10.1145/3437992.3439916

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

Publisher's Version Published Artifact Artifacts Available Article: poplws21cppmain-p22-p doi:10.1145/3437992.3439923

Program Logics

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

Publisher's Version Published Artifact Artifacts Available Article: poplws21cppmain-p36-p doi:10.1145/3437992.3439930

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

Publisher's Version Published Artifact Artifacts Available Article: poplws21cppmain-p39-p doi:10.1145/3437992.3439931

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 Published Artifact Artifacts Available Article: poplws21cppmain-p53-p doi:10.1145/3437992.3439934

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 Article: poplws21cppmain-p26-p doi:10.1145/3437992.3439924

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

Publisher's Version Article: poplws21cppmain-p32-p doi:10.1145/3437992.3439929

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 Article: poplws21cppmain-p19-p doi:10.1145/3437992.3439920

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 Article: poplws21cppmain-p3-p doi:10.1145/3437992.3439913

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 Published Artifact Artifacts Available Article: poplws21cppmain-p8-p doi:10.1145/3437992.3439914

Proof Tactics

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

Publisher's Version Published Artifact Artifacts Available Article: poplws21cppmain-p31-p doi:10.1145/3437992.3439928

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 Article: poplws21cppmain-p27-p doi:10.1145/3437992.3439925

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 Article: poplws21cppmain-p2-p doi:10.1145/3437992.3439912

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 Article: poplws21cppmain-p60-p doi:10.1145/3437992.3439935

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 Article: poplws21cppmain-p17-p doi:10.1145/3437992.3439918

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 Article: poplws21cppmain-p18-p doi:10.1145/3437992.3439919

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 Article: poplws21cppmain-p44-p doi:10.1145/3437992.3439933

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

Publisher's Version Article: poplws21cppmain-p20-p doi:10.1145/3437992.3439921

Logic, Set Theory, and Category Theory

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

Publisher's Version Published Artifact Artifacts Available Article: poplws21cppmain-p28-p doi:10.1145/3437992.3439926

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

Publisher's Version Article: poplws21cppmain-p40-p doi:10.1145/3437992.3439932

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

Publisher's Version Published Artifact Artifacts Available Article: poplws21cppmain-p21-p doi:10.1145/3437992.3439922

proc time: 0.04