POPL 2023 Co-Located Events
POPL 2023 Co-Located Events
Powered by
Conference Publishing Consulting

12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), January 16-17, 2023, Boston, MA, USA

CPP 2023 – Proceedings

Contents - Abstracts - Authors

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


Title Page
Welcome from the Chairs
CPP 2023 Organization
CPP 2023 Supporters


CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)
Sandrine Blazy ORCID logo
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
Publisher's Version
Improved Assistance for Interactive Proof (Keynote)
Cezary Kaliszyk ORCID logo
(University of Innsbruck, Austria)
Publisher's Version


Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Reynald Affeldt ORCID logo, Cyril Cohen ORCID logo, and Ayumu Saito ORCID logo
(AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan)
Publisher's Version
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon ORCID logo, Quentin Canu ORCID logo, and Pierre-Yves Strub ORCID logo
(Inria, France; École Polytechnique, France; Meta, France)
Publisher's Version
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu ORCID logo, Tahina Ramananandro ORCID logo, Aseem Rastogi ORCID logo, Nikhil Swamy ORCID logo, Aymeric Fromherz ORCID logo, Kesha HietalaORCID logo, Bryan ParnoORCID logo, and Ravi Ramamurthy ORCID logo
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
Publisher's Version Info
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne BaanenORCID logo, Alex J. Best ORCID logo, Nirvana Coppola ORCID logo, and Sander R. Dahmen ORCID logo
(Vrije Universiteit Amsterdam, Netherlands)
Publisher's Version Info
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau ORCID logo, Enzo Crance ORCID logo, Louise Dubois de Prisque ORCID logo, Chantal KellerORCID logo, Assia Mahboubi ORCID logo, 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
Encoding Dependently-Typed Constructions into Simple Type Theory
Anthony Bordg ORCID logo and Adrián Doña Mateo ORCID logo
(University of Cambridge, UK; University of Edinburgh, UK)
Publisher's Version
A Formalized Reduction of Keller’s Conjecture
Joshua Clune ORCID logo
(Carnegie Mellon University, USA)
Publisher's Version
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt ORCID logo, Robert AtkeyORCID logo, Wen Kokke ORCID logo, Ekaterina Komendantskaya ORCID logo, and Luca Arnaboldi ORCID logo
(Heriot-Watt University, UK; University of Strathclyde, UK; University of Edinburgh, UK)
Publisher's Version Info
Formalising the h-Principle and Sphere Eversion
Floris van Doorn ORCID logo, Patrick Massot ORCID logo, and Oliver Nash ORCID logo
(University of Paris-Saclay, France; CNRS, France; Imperial College London, UK)
Publisher's Version Published Artifact Info Artifacts Available
Terms for Efficient Proof Checking and Parsing
Michael FärberORCID logo
(University of Innsbruck, Austria)
Publisher's Version
Formalizing and Computing Propositional Quantifiers
Hugo Férée ORCID logo and Sam van Gool ORCID logo
(Université Paris Cité, France)
Publisher's Version Info
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster ORCID logo, Felix Jahn ORCID logo, and Gert Smolka ORCID logo
(Inria, France; Saarland University, Germany)
Publisher's Version
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi
Benjamin Grégoire ORCID logo, Jean-Christophe Léchenet ORCID logo, and Enrico Tassi ORCID logo
(Université Côte d’Azur, France; Inria, France)
Publisher's Version
Mechanised Semantics for Gated Static Single Assignment
Yann HerklotzORCID logo, Delphine Demange ORCID logo, and Sandrine Blazy ORCID logo
(Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
Publisher's Version
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl ORCID logo and Aart MiddeldorpORCID logo
(University of Innsbruck, Austria)
Publisher's Version Info
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian ORCID logo, Yong Kiam Tan ORCID logo, and André Platzer ORCID logo
(Carnegie Mellon University, USA; KIT, Germany)
Publisher's Version
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki Koutsoukou-Argyraki ORCID logo, Mantas Bakšys ORCID logo, and Chelsea Edmonds ORCID logo
(University of Cambridge, UK)
Publisher's Version
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux ORCID logo, Axel Ljungström ORCID logo, and Anders MörtbergORCID logo
(University of Paris-Saclay, France; ENS Paris-Saclay, France; Stockholm University, Sweden)
Publisher's Version
Aesop: White-Box Best-First Proof Search for Lean
Jannis LimpergORCID logo and Asta Halkjær From ORCID logo
(Vrije Universiteit Amsterdam, Netherlands; DTU, Denmark)
Publisher's Version
Formalising Sharkovsky’s Theorem (Proof Pearl)
Bhavik Mehta ORCID logo
(University of Cambridge, UK)
Publisher's Version Info
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni ORCID logo, Antoine Delignat-Lavaud ORCID logo, Cédric Fournet ORCID logo, Tahina Ramananandro ORCID logo, and Nikhil Swamy ORCID logo
(Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA)
Publisher's Version
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen ORCID logo, Danil AnnenkovORCID logo, and Bas Spitters ORCID logo
(Aarhus University, Denmark)
Publisher's Version
P4Cub: A Little Language for Big Routers
Rudy Peterson ORCID logo, Eric Hayden Campbell ORCID logo, John Chen ORCID logo, Natalie Isak ORCID logo, Calvin Shyu ORCID logo, Ryan Doenges ORCID logo, Parisa Ataei ORCID logo, and Nate FosterORCID logo
(Cornell University, USA; Microsoft, USA)
Publisher's Version Published Artifact Artifacts Available
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb ORCID logo, Ian J. HayesORCID logo, and Mark Utting ORCID logo
(University of Queensland, Australia)
Publisher's Version
A Formalization of Doob’s Martingale Convergence Theorems in mathlib
Kexing Ying ORCID logo and Rémy Degenne ORCID logo
(University of Cambridge, UK; University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9198-CRIStAL, France)
Publisher's Version

proc time: 4.66