CPP 2026
as the organisers put it
Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education. CPP is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. CPP 2026 will be held in January 2026 and will be co-located with POPL 2026 in Rennes, France.
who it's for
formal methods researchers, theorem prover developers, proof assistant users, verification tool developers, programming language researchers, distributed systems researchers
topics
formalization of universal divided power algebra; normalization-by-evaluation typechecking in MLTT; compositional cache coherence proofs (MSI/MI/SI); confluence for actor-based systems; physical-step modality for step-indexed logics; symbolic finite transducers in Isabelle/HOL; logical pinning for container-internal pointers; distribution typeclass for certified random samplers; Rocq-certified decision procedures for one-relation monoids; mechanized dominator tree certification; verified VCG and compiler for Dafny; cylindrical algebraic decomposition in Coq/Rocq
| title | author | length |
|---|---|---|
| Formalizing polynomial laws and the universal divided power algebra | Antoine Chambert-Loir, María Inés de Frutos-Fernández | 20m |
Formalization in Lean/Mathlib of polynomial laws and the first steps of Roby’s universal divided power algebra constructs the graded algebra and a partial… | ||
| A Certifying Proof Assistant for Synthetic Mathematics in Lean | Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey | 22m |
SynthLean embeds a deep embedding of Martin-Löf type theory as a DSL inside Lean and implements certifying normalization-by-evaluation typechecking that emits… | ||
| Towards composable proofs of cache coherence protocols | Martina Camaioni, Yann Herklotz, Tz-Ching Yu, Thomas Bourgeat | 21m |
Proposes a compositional proof that MSI refines the combination of MI and SI, formalized in Lean 4, cutting required invariants from hundreds to just 15 by… | ||
| Layers of Confluence for Actors | Ludovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, Yannick Zakowski | 22m |
Presents a concrete proof technique that adapts de Bruijn’s induction-style confluence proof to indexed transition systems and a weak diamond property (D1/D2)… | ||
| Building Blocks for Step-Indexed Program Logics | Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers | 22m |
Claims a single modular physical-step modality lets program-logic designers recover every prior multiple-later elimination technique without redoing… | ||
| Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis | Shuanglong Kan, Anthony W. Lin | 25m |
First formalization of symbolic finite transducers and core algorithms in Isabelle/HOL, using an abstract Boolean-algebra label layer plus refinement to… | ||
| Precise Reasoning about Container-Internal Pointers with Logical Pinning | Yawen Guan, Clément Pit-Claudel | 23m |
Claims a lightweight borrowing discipline called logical pinning that decouples address exposure from ownership so container-internal pointers can be tracked… | ||
| Modular Specifications and Implementations of Random Samplers in Higher-Order Separation(…) | Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal | 23m |
Defines a reusable distribution typeclass for Eris (Iris-based) that internalizes sampler reasoning, proves a distribution adequacy theorem linking the logical… | ||
| Certifying the decidability of the word problem in monoids at large | Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith | 24m |
Implements a Rocq-based toolbox that uses Rocq proof assistant certificates and proofs-by-reflection guided by an external oracle to certify decision… | ||
| A Rose Tree is Blooming (Proof Pearl) | Joomy Korkut | 16m |
Compares two implementations of rose-tree unfolding in the Rocq prover: an inductive version requiring a well‑founded relation and accessibility proofs, and a… | ||
| Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust | Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan | 21m |
Creusot gains support for linear ghost resources and implements a ptr_own with permission map that lets mutable borrows be expressed and borrow‑checked in… | ||
| Mechanized Dominator Tree Certification | Jean-Christophe Léchenet | 21m |
Claims a verified validator of fast dominator computation: an unverified implementation (Lengauer–Tarjan variant instrumented to emit a numbering) plus a low… | ||
| Business Meeting | Nikhil Swamy, Nicolas Tabareau | 30m |
Conference sees 178 registrations, the highest yet; program runs from 75 submissions with 27 accepted (about 36%), up from 51 last year. Review process uses a… | ||
| Can we formalise type theory intrinsically without any compromise? A case study in(…) | Liang-Ting Chen, Fredrik Nordvall Forsberg, Tzu-Chun Tsai | 23m |
An intrinsic syntax for dependent type theory is encoded in Cubical Agda using quotient inductive-inductive-recursive types to define the initial natural model… | ||
| A Recipe for Modular Verification of Generic Tree Traversals | Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg | 22m |
Presents a concrete verification recipe that models traversal state with a zipper with shadow and characterizes step types as action and silent steps, yielding… | ||
| Formalization of a Proof Calculus for Incremental Linearization for Satisfiability(…) | Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark Barrett, Cesare Tinelli | 22m |
Formalizes the incremental linearization proof calculus used by cvc5 inside Lean, extends the lean-smt plugin, and proves soundness of 21 proof rules… | ||
| Mechanizing Synthetic Tait Computability in Istari | Runming Li, Yue Yao, Robert Harper | 22m |
Mechanization of Synthetic Tait Computability is formalized in the Istari extensional type theory with equality reflection, producing a reusable library of… | ||
| Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq | Holger Thies | 22m |
Formalizes a verified solver in Rocq that computes Taylor-series solutions for multivariate analytic ODE initial value problems following the… | ||
| How can Machine Learning Help Formal Proving ? | Amaury Hayat | 01h 02m |
Reviews recent progress using Lean mathlib (~300k theorems) and pre‑trained LMs fine‑tuned for proving, combines reinforcement learning (AlphaZero‑style) with… | ||
| Adhesive Category Theory for Graph Rewriting in Rocq | Samuel Arsac, Russ Harmer, Damien Pous | 21m |
A Rocq library implements adhesive and weaker RM and RMU adhesive category hierarchies using Hierarchy Builder and encodes morphism hierarchies (mono, reg… | ||
| Specification, Semantics, and Verification of Quantum Programs | Jennifer Paykin | 53m |
Survey of methods claims that circuit semantics are handled as density matrices/mixed states to make execution deterministic, that SMT‑style and tableau… | ||
| Cylindrical Algebraic Decomposition in Coq/Rocq | Quentin Vermande | 18m |
Formalizes correctness of Cylindrical Algebraic Decomposition in Coq/Rocq, proving: for any finite family of polynomials in n variables there exists a CAD… | ||
| Enhancing Symbolic Execution with Machine-Checked Safety Proofs | David Trabish, Shachar Itzhaky | 21m |
Generates machine-checked safety proofs per-analysis so an exhaustive symbolic run yields a Rocq-verified proof tying symbolic to concrete LLVM IR semantics… | ||
| Verified VCG and Verified Compiler for Dafny | Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan | 21m |
Builds a functional big‑step semantics for an imperative subset of Dafny and proves a verified VCG and verified compiler that translate Dafny (mutual… | ||
| A Lambda-Superposition Tactic for Isabelle/HOL | Massin Guerdi | 22m |
A new Isabelle/HOL tactic implements the λ-superposition calculus to avoid Metis’s first‑order encodings, runs proof search on Isabelle terms, and reconstructs… | ||
| Higher order differential calculus in Mathlib | Sébastien Gouëzel | 26m |
A higher‑order differential calculus library is implemented in Mathlib using Lean that supports arbitrary scalar fields, functions on domains (not only open… | ||
| nothing matches | ||