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)

Frontmatter

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

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
Improved Assistance for Interactive Proof (Keynote)
Cezary Kaliszyk
(University of Innsbruck, Austria)
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)
Publisher's Version
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon, Quentin Canu, and Pierre-Yves Strub
(Inria, France; École Polytechnique, France; Meta, France)
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)
Publisher's Version Info
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 Info
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
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
A Formalized Reduction of Keller’s Conjecture
Joshua Clune
(Carnegie Mellon University, USA)
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)
Publisher's Version Info
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 Info Artifacts Available
Terms for Efficient Proof Checking and Parsing
Michael Färber
(University of Innsbruck, Austria)
Publisher's Version
Formalizing and Computing Propositional Quantifiers
Hugo Férée and Sam van Gool
(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, Felix Jahn, and Gert Smolka
(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, Jean-Christophe Léchenet, and Enrico Tassi
(Université Côte d’Azur, France; Inria, France)
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)
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)
Publisher's Version Info
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
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
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
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
Formalising Sharkovsky’s Theorem (Proof Pearl)
Bhavik Mehta
(University of Cambridge, UK)
Publisher's Version Info
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
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters
(Aarhus University, Denmark)
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)
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)
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)
Publisher's Version

proc time: 3.98