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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 Article: poplws21cppmain-p36-p doi:10.1145/3437992.3439930

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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 Article: poplws21cppmain-p8-p doi:10.1145/3437992.3439914

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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 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)


@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 Article: poplws21cppmain-p21-p doi:10.1145/3437992.3439922

proc time: 0.05