CPP 2025
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 2025 will be held in January 2025 and will be co-located with POPL 2025 in Denver, Colorado, United States.
who it's for
theorem prover users, proof assistant developers, formal methods researchers, verification tool authors, programming languages researchers, security engineers, systems verification engineers
topics
Isabelle/HOL formalizations; Coq executable semantics; Lean 4 certificates; Cubical Agda correctness; formalized Burrows-Wheeler transform; CertiCoq WebAssembly backend; leakage-free Jasmin proofs; CHERI C memory model; differential privacy in Isabelle/HOL; Aesop tactic script optimization; concurrency memory models with CTrees; confluence of term rewriting
| title | author | length |
|---|---|---|
| Formalized Burrows-Wheeler Transform | Louis Cheung, Alistair Moffat, Christine Rizkallah | 31m |
First mechanized verification of the Burrows‑Wheeler transform and its inverse, formalized in Isabelle/HOL and proven correct, invertible, and terminating; two… | ||
| Certifying rings of integers in number fields | Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen | 28m |
Lean 4 formalization certifies explicit integral bases and discriminants for number fields by having SageMath generate SageMath → Lean certificates that the… | ||
| Leakage-Free Probabilistic Jasmin Programs | José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh | 24m |
Presents a new semantic characterization of leakage-freeness for probabilistic Jasmin programs and proves it equivalent to a probabilistic relational Hoare… | ||
| Prospects for Computer Formalization of Infinite-Dimensional Category Theory | Emily Riehl | 01h 00m |
Goal is to formalize Joyal–Lurie ∞-category theory; two active efforts use different strategies: Infinity Cosmos in Lean (analytic/axiomatic layer built in… | ||
| Tactic Script Optimisation for Aesop | Jannis Limperg | 30m |
Generates an optimized Lean tactic script from Aesop output using a three-stage pipeline (local dynamic optimization, structuring with static and dynamic… | ||
| The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic | Simon Friis Vindum, Aina Linn Georges, Lars Birkedal | 22m |
Proposes a new modality that permits non-frame-preserving updates to ghost state inside Iris, formalizes a parameterized stack-cutting transformation that… | ||
| Intrinsically Correct Sorting in Cubical Agda | Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide | 27m |
Claims intrinsic correctness of bialgebraic sorting follows solely from a distributive law lifted to an indexed setting; implementation uses Cubical Agda with… | ||
| Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems | Christina Kirk, Aart Middeldorp | 28m |
Formalizes Okui’s 1998 sufficient condition for confluence of left‑linear term rewrite systems inside Isabelle/HOL, representing multisteps as proof terms… | ||
| Machine Checked Proofs and Programs in Algebraic Combinatorics | Florent Hivert | 30m |
A Coq/Mathematical Components library formalizes symmetric functions and character theory, delivering a proof of the Littlewood-Richardson rule by symbolically… | ||
| An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting | Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada | 31m |
Isabelle/HOL formalizes co-rewrite pairs and integrates polynomial interpretations over negative integers, the weighted path order and the co-WPO variant so… | ||
| Verified and Efficient Matching of Regular Expressions with Lookaround | Agnishom Chattopadhyay, Angela W. Li, Konstantinos Mamouras | 29m |
Presents a Coq formalization and a verified matcher that handles lookahead and lookbehind, including negative lookarounds via two complementary predicates, and… | ||
| Monadic interpreters for concurrent memory models: Executable semantics of a concurrent(…) | Nicolas Chappe, Ludovic Henrio, Yannick Zakowski | 30m |
Defines an executable, layered semantics for a concurrent subset of LLVM IR implemented in Coq using CTrees and extracted to OCaml; builds an interleaving… | ||
| An Isabelle/HOL Framework for Synthetic Completeness Proofs | Asta Halkjær From | 31m |
Mechanization in Isabelle/HOL encodes a transfinite Lindenbaum construction that builds maximal consistent sets from any consistency predicate satisfying… | ||
| Formally verified hardening of C programs against hardware fault injection | Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet | 34m |
Implements two control-flow hardening transforms over CompCert RTL and proves two properties in Coq proofs: semantic preservation (no behavior change without… | ||
| Formalization of Differential Privacy in Isabelle/HOL | Tetsuya Sato, Yasuhiko Minamide | 30m |
Provides a reusable Isabelle/HOL library that formalizes differential privacy over continuous probability distributions, including the standard ε,δ definition… | ||
| Business Meeting | Sandrine Blazy, Nicolas Tabareau | 11m |
About 51 papers are submitted and 20 accepted this year, reviewed by 32 PC members with 26 external reviewers and two months for reviews and rebuttals; reviews… | ||
| CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq | Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters | 30m |
A verified backend implemented and proven in Coq generates WebAssembly modules from CertiCoq’s Lambda ANF, mechanised against WasmCert-Coq and offering a… | ||
| Split Decisions: Explicit Contexts for Substructural Languages | Daniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka | 28m |
Contexts as Resource Vectors frames contexts as lists whose entries carry tags from a resource algebra so consumption means changing tags rather than removing… | ||
| Further Tackling Post Correspondence Problem and Proof Generation | Akihiro Omori, Yasuhiko Minamide | 31m |
Claim: all but two PCP[3,4] instances are decided — 368 instances solved — using two new invariant-finding methods plus a manual invariant editor; one method… | ||
| CRIS: The power of imagination in specification and verification | Chung-Kil Hur | 01h 03m |
CRIS introduces imaginary nondeterminism to let specifications include angelic choices and mix operational steps with separation logic, implemented on top of… | ||
| Formalizing the One-way to Hiding Theorem | Katharina Heidler, Dominique Unruh | 24m |
Formalizes the One-way to Hiding (O2H) theorem inside Isabelle, proving the semi-classical O2H variants and providing a novel, simpler mixed-state proof while… | ||
| A CHERI C Memory Model for Verified Temporal Safety | Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell | 27m |
Defines a CHERI C object memory model that implements a new PNVI-CHERI provenance scheme, encodes five revocation strategies, and plugs into the Cerberus… | ||
| Nominal Matching Logic With Fixpoints | Mircea Sebe, Maribel Fernandez, James Cheney | 30m |
Extends nominal matching logic by adding mu fixed-point operator and set variables to derive an alpha-structural induction principle for any nominal binding… | ||
| nothing matches | ||