CPP 2023 – Proceedings

12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023)

Frontmatter

Keynotes

CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)
Sandrine Blazy
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)


@InProceedings{CPP23p1, author = {Sandrine Blazy}, title = {CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3573105.3579107}, year = {2023}, } Publisher's Version

Improved Assistance for Interactive Proof (Keynote)
Cezary Kaliszyk
(University of Innsbruck, Austria)


@InProceedings{CPP23p23, author = {Cezary Kaliszyk}, title = {Improved Assistance for Interactive Proof (Keynote)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {23-22}, doi = {10.1145/3573105.3579108}, year = {2023}, } Publisher's Version

Papers

Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Reynald Affeldt, Cyril Cohen, and Ayumu Saito
(AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan)


@InProceedings{CPP23p45, author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito}, title = {Semantics of Probabilistic Programs using s-Finite Kernels in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {45-44}, doi = {10.1145/3573105.3575691}, year = {2023}, } Publisher's Version

A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon, Quentin Canu, and Pierre-Yves Strub
(Inria, France; École Polytechnique, France; Meta, France)


@InProceedings{CPP23p67, author = {Xavier Allamigeon and Quentin Canu and Pierre-Yves Strub}, title = {A Formal Disproof of Hirsch Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {67-66}, doi = {10.1145/3573105.3575678}, year = {2023}, } Publisher's Version

FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)


@InProceedings{CPP23p89, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {89-88}, doi = {10.1145/3573105.3575687}, year = {2023}, } Publisher's Version

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen, Alex J. Best, Nirvana Coppola, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands)


@InProceedings{CPP23p111, author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen}, title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {111-110}, doi = {10.1145/3573105.3575682}, year = {2023}, } Publisher's Version

Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)


@InProceedings{CPP23p133, author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial}, title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {133-132}, doi = {10.1145/3573105.3575676}, year = {2023}, } Publisher's Version

Encoding Dependently-Typed Constructions into Simple Type Theory
Anthony Bordg and Adrián Doña Mateo
(University of Cambridge, UK; University of Edinburgh, UK)


@InProceedings{CPP23p155, author = {Anthony Bordg and Adrián Doña Mateo}, title = {Encoding Dependently-Typed Constructions into Simple Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {155-154}, doi = {10.1145/3573105.3575679}, year = {2023}, } Publisher's Version

A Formalized Reduction of Keller’s Conjecture
Joshua Clune
(Carnegie Mellon University, USA)


@InProceedings{CPP23p177, author = {Joshua Clune}, title = {A Formalized Reduction of Keller’s Conjecture}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {177-176}, doi = {10.1145/3573105.3575669}, year = {2023}, } Publisher's Version

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi
(Heriot-Watt University, UK; University of Strathclyde, UK; University of Edinburgh, UK)


@InProceedings{CPP23p199, author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi}, title = {Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {199-198}, doi = {10.1145/3573105.3575674}, year = {2023}, } Publisher's Version

Formalising the h-Principle and Sphere Eversion
Floris van Doorn, Patrick Massot, and Oliver Nash
(University of Paris-Saclay, France; CNRS, France; Imperial College London, UK)


@InProceedings{CPP23p221, author = {Floris van Doorn and Patrick Massot and Oliver Nash}, title = {Formalising the h-Principle and Sphere Eversion}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {221-220}, doi = {10.1145/3573105.3575688}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available

Terms for Efficient Proof Checking and Parsing
Michael Färber
(University of Innsbruck, Austria)


@InProceedings{CPP23p243, author = {Michael Färber}, title = {Terms for Efficient Proof Checking and Parsing}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {243-242}, doi = {10.1145/3573105.3575686}, year = {2023}, } Publisher's Version

Formalizing and Computing Propositional Quantifiers
Hugo Férée and Sam van Gool
(Université Paris Cité, France)


@InProceedings{CPP23p265, author = {Hugo Férée and Sam van Gool}, title = {Formalizing and Computing Propositional Quantifiers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {265-264}, doi = {10.1145/3573105.3575668}, year = {2023}, } Publisher's Version

A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster, Felix Jahn, and Gert Smolka
(Inria, France; Saarland University, Germany)


@InProceedings{CPP23p287, author = {Yannick Forster and Felix Jahn and Gert Smolka}, title = {A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {287-286}, doi = {10.1145/3573105.3575690}, year = {2023}, } Publisher's Version

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi
Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi
(Université Côte d’Azur, France; Inria, France)


@InProceedings{CPP23p309, author = {Benjamin Grégoire and Jean-Christophe Léchenet and Enrico Tassi}, title = {Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {309-308}, doi = {10.1145/3573105.3575683}, year = {2023}, } Publisher's Version

Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz, Delphine Demange, and Sandrine Blazy
(Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France)


@InProceedings{CPP23p331, author = {Yann Herklotz and Delphine Demange and Sandrine Blazy}, title = {Mechanised Semantics for Gated Static Single Assignment}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {331-330}, doi = {10.1145/3573105.3575681}, year = {2023}, } Publisher's Version

A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl and Aart Middeldorp
(University of Innsbruck, Austria)


@InProceedings{CPP23p353, author = {Christina Kohl and Aart Middeldorp}, title = {A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {10.1145/3573105.3575667}, year = {2023}, } Publisher's Version

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, and André Platzer
(Carnegie Mellon University, USA; KIT, Germany)


@InProceedings{CPP23p375, author = {Katherine Kosaian and Yong Kiam Tan and André Platzer}, title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {375-374}, doi = {10.1145/3573105.3575672}, year = {2023}, } Publisher's Version

A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
(University of Cambridge, UK)


@InProceedings{CPP23p397, author = {Angeliki Koutsoukou-Argyraki and Mantas Bakšys and Chelsea Edmonds}, title = {A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {397-396}, doi = {10.1145/3573105.3575680}, year = {2023}, } Publisher's Version

Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux, Axel Ljungström, and Anders Mörtberg
(University of Paris-Saclay, France; ENS Paris-Saclay, France; Stockholm University, Sweden)


@InProceedings{CPP23p419, author = {Thomas Lamiaux and Axel Ljungström and Anders Mörtberg}, title = {Computing Cohomology Rings in Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {419-418}, doi = {10.1145/3573105.3575677}, year = {2023}, } Publisher's Version

Aesop: White-Box Best-First Proof Search for Lean
Jannis Limperg and Asta Halkjær From
(Vrije Universiteit Amsterdam, Netherlands; DTU, Denmark)


@InProceedings{CPP23p441, author = {Jannis Limperg and Asta Halkjær From}, title = {Aesop: White-Box Best-First Proof Search for Lean}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {441-440}, doi = {10.1145/3573105.3575671}, year = {2023}, } Publisher's Version

Formalising Sharkovsky’s Theorem (Proof Pearl)
Bhavik Mehta
(University of Cambridge, UK)


@InProceedings{CPP23p463, author = {Bhavik Mehta}, title = {Formalising Sharkovsky’s Theorem (Proof Pearl)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {463-462}, doi = {10.1145/3573105.3575689}, year = {2023}, } Publisher's Version

ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, and Nikhil Swamy
(Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA)


@InProceedings{CPP23p485, author = {Haobin Ni and Antoine Delignat-Lavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy}, title = {ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {485-484}, doi = {10.1145/3573105.3575684}, year = {2023}, } Publisher's Version

Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters
(Aarhus University, Denmark)


@InProceedings{CPP23p507, author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters}, title = {Formalising Decentralised Exchanges in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {507-506}, doi = {10.1145/3573105.3575685}, year = {2023}, } Publisher's Version

P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)


@InProceedings{CPP23p529, author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster}, title = {P4Cub: A Little Language for Big Routers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {529-528}, doi = {10.1145/3573105.3575670}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available

Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb, Ian J. Hayes, and Mark Utting
(University of Queensland, Australia)


@InProceedings{CPP23p551, author = {Brae J. Webb and Ian J. Hayes and Mark Utting}, title = {Verifying Term Graph Optimizations using Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {551-550}, doi = {10.1145/3573105.3575673}, year = {2023}, } Publisher's Version

A Formalization of Doob’s Martingale Convergence Theorems in mathlib
Kexing Ying and Rémy Degenne
(University of Cambridge, UK; University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9198-CRIStAL, France)


@InProceedings{CPP23p573, author = {Kexing Ying and Rémy Degenne}, title = {A Formalization of Doob’s Martingale Convergence Theorems in mathlib}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {573-572}, doi = {10.1145/3573105.3575675}, year = {2023}, } Publisher's Version

proc time: 0.04