CPP 2026 – Proceedings

15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2026)

Frontmatter

Formalized Mathematics

Higher Order Differential Calculus in Mathlib
Sébastien Gouëzel
(CNRS - Rennes University, France)

Publisher's Version ACM SIGPLAN Distinguished Paper Award

Bar Inductive Predicates for Constructive Algebra in Rocq
Dominique Larchey-Wendling
(Université de Lorraine - LORIA, France; CNRS, France)

Publisher's Version

Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
Holger Thies
(Kyoto University, Japan)

Publisher's Version Published Artifact Artifacts Available

Cylindrical Algebraic Decomposition in Coq/Rocq
Quentin Vermande
(Université Côte d’Azur - Inria, France)

Publisher's Version

Adhesive Category Theory for Graph Rewriting in Rocq
Samuel Arsac, Russ Harmer, and Damien Pous
(ENS Lyon - CNRS - UCBL1 - LIP - Plume team - UMR 5668, France; CNRS - ENS de Lyon - UCBL1 - LIP - Plume team - UMR 5668, France)

Publisher's Version Published Artifact Artifacts Available

Formalizing Polynomial Laws and the Universal Divided Power Algebra
Antoine Chambert-Loir and María Inés de Frutos-Fernández
(Université Paris Cité, France; University of Bonn, Germany)

Publisher's Version Published Artifact Artifacts Available

Proof Assistants

A Certifying Proof Assistant for Synthetic Mathematics in Lean
Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, and Steve Awodey
(Carnegie Mellon University, USA; Chalmers University of Technology, Sweden; LMU Munich, Germany; Chapman University, USA; Stockholm University, Sweden)

Publisher's Version Published Artifact Artifacts Available

Adding Sorts to an Isabelle Formalization of Superposition
Balazs Toth, Martin Desharnais-Schäfer, and Jasmin Blanchette
(LMU Munich, Germany)

Publisher's Version

A Lambda-Superposition Tactic for Isabelle/HOL
Massin Guerdi
(LMU Munich, Germany)

Publisher's Version

Certifying the Decidability of the Word Problem in Monoids at Large
Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, and Finn Smith
(Nantes Université - École Centrale Nantes - CNRS - Inria - LS2N - UMR 6004, France; Université Paris-Saclay - CNRS - ENS Paris Saclay - Inria - LMF, France; Vrije Universiteit Amsterdam, Netherlands; St Andrews University, UK)

Publisher's Version

Compilers

Mechanized Dominator Tree Certification
Jean-Christophe Léchenet
(Université Côte d’Azur - Inria, France)

Publisher's Version Published Artifact Artifacts Available ACM SIGPLAN Distinguished Paper Award

Brack: A Verified Compiler for Scheme via CakeML
Pascal Y. Lasnier, Jeremy Yallop, and Magnus O. Myreen
(University of Cambridge, UK; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)

Publisher's Version Published Artifact Artifacts Available

Verified VCG and Verified Compiler for Dafny
Daniel Nezamabadi, Magnus O. Myreen, and Yong Kiam Tan
(ETH Zurich, Switzerland; Chalmers University of Technology - University of Gothenburg, Sweden; A*STAR, Singapore; Nanyang Technological University, Singapore)

Publisher's Version

Foundational Verification of Running-Time Bounds for Interactive Programs
Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, and Adam Chlipala
(Massachusetts Institute of Technology, USA; Carnegie Mellon University, USA; Google, USA; ETH Zurich, Switzerland)

Publisher's Version

Metatheory

Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda
Liang-Ting Chen, Fredrik Nordvall Forsberg, and Tzu-Chun Tsai
(Academia Sinica, Taiwan; University of Strathclyde, UK)

Publisher's Version Published Artifact Info Artifacts Available

Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark Barrett, and Cesare Tinelli
(Federal University of Minas Gerais, Brazil; Stanford University, USA; University of Iowa, USA)

Publisher's Version Published Artifact Artifacts Available

Mechanizing Synthetic Tait Computability in Istari
Runming Li, Yue Yao, and Robert Harper
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available

Building Blocks for Step-Indexed Program Logics
Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Aalborg University, Denmark; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available

A Rose Tree Is Blooming (Proof Pearl)
Joomy Korkut
(Bloomberg, USA)

Publisher's Version

Program Verification

Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
Shuanglong Kan and Anthony W. Lin
(Barkhausen Institute, Germany; MPI-SWS, Germany; TU Kaiserslautern, Germany)

Publisher's Version

Enhancing Symbolic Execution with Machine-Checked Safety Proofs
David Trabish and Shachar Itzhaky
(Technion, Israel)

Publisher's Version

Layers of Confluence for Actors
Ludovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, and Yannick Zakowski
(CNRS, France; University of Oslo, Norway; Western Norway University of Applied Sciences, Norway; Inria, France)

Publisher's Version Published Artifact Artifacts Available

Towards Composable Proofs of Cache Coherence Protocols
Martina Camaioni, Yann Herklotz, Tz-Ching Yu, and Thomas Bourgeat
(EPFL, Switzerland)

Publisher's Version Published Artifact Artifacts Available

Separation Logic

A Recipe for Modular Verification of Generic Tree Traversals
Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, and Deepak Garg
(MPI-SWS, Germany; IST Austria, Austria; Radboud University Nijmegen, Netherlands)

Publisher's Version Published Artifact Artifacts Available

Precise Reasoning about Container-Internal Pointers with Logical Pinning
Yawen Guan and Clément Pit-Claudel
(EPFL, Switzerland)

Publisher's Version Published Artifact Artifacts Available ACM SIGPLAN Distinguished Paper Award

Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, and Lars Birkedal
(ENS Rennes, France; ENS Paris-Saclay, France; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available

Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
Arnaud Golfouse, Armaël Guéneau, and Jacques-Henri Jourdan
(Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - Laboratoire Méthodes Formelles, France; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Laboratoire Méthodes Formelles, France)

Publisher's Version

proc time: 0.83