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)

Publisher's Version Article: poplws23cppmain-key1-p doi:10.1145/3573105.3579107

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

Publisher's Version Article: poplws23cppmain-key2-p doi:10.1145/3573105.3579108

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)

Publisher's Version Article: poplws23cppmain-p61-p doi:10.1145/3573105.3575691

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

Publisher's Version Article: poplws23cppmain-p29-p doi:10.1145/3573105.3575678

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)

Publisher's Version Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687

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)

Publisher's Version Article: poplws23cppmain-p36-p doi:10.1145/3573105.3575682

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)

Publisher's Version Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676

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

Publisher's Version Article: poplws23cppmain-p30-p doi:10.1145/3573105.3575679

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

Publisher's Version Article: poplws23cppmain-p10-p doi:10.1145/3573105.3575669

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)

Publisher's Version Article: poplws23cppmain-p21-p doi:10.1145/3573105.3575674

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)

Publisher's Version Published Artifact Artifacts Available Article: poplws23cppmain-p53-p doi:10.1145/3573105.3575688

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

Publisher's Version Article: poplws23cppmain-p44-p doi:10.1145/3573105.3575686

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

Publisher's Version Article: poplws23cppmain-p2-p doi:10.1145/3573105.3575668

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)

Publisher's Version Article: poplws23cppmain-p58-p doi:10.1145/3573105.3575690

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)

Publisher's Version Article: poplws23cppmain-p37-p doi:10.1145/3573105.3575683

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)

Publisher's Version Article: poplws23cppmain-p32-p doi:10.1145/3573105.3575681

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

Publisher's Version Article: poplws23cppmain-p1-p doi:10.1145/3573105.3575667

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)

Publisher's Version Article: poplws23cppmain-p19-p doi:10.1145/3573105.3575672

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)

Publisher's Version Article: poplws23cppmain-p31-p doi:10.1145/3573105.3575680

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)

Publisher's Version Article: poplws23cppmain-p27-p doi:10.1145/3573105.3575677

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

Publisher's Version Article: poplws23cppmain-p18-p doi:10.1145/3573105.3575671

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

Publisher's Version Article: poplws23cppmain-p57-p doi:10.1145/3573105.3575689

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)

Publisher's Version Article: poplws23cppmain-p38-p doi:10.1145/3573105.3575684

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

Publisher's Version Article: poplws23cppmain-p40-p doi:10.1145/3573105.3575685

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)

Publisher's Version Published Artifact Artifacts Available Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670

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

Publisher's Version Article: poplws23cppmain-p20-p doi:10.1145/3573105.3575673

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)

Publisher's Version Article: poplws23cppmain-p22-p doi:10.1145/3573105.3575675

proc time: 0.05