CPP 2023
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 2023 will be held on 16-17 January 2023 and will be co-located with POPL 2023 in Boston, Massachusetts, United States.
| title | author | length |
|---|---|---|
| Terms for Efficient Proof Checking and Parsing | Michael Färber | 19m |
Implementation in Rust (the proof checker Kontroli) introduces heterogeneous terms that separate long-lived global terms from short-lived local terms and uses… | ||
| Compositional pre-processing for automated reasoning in dependent type theory | Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial | 21m |
Implements compositional, small-step goal transforms for Coq that systematically convert inductives, uninterpreted symbols and higher-order/dependent… | ||
| Practical and sound equality tests, automatically | Benjamin Gregoire, Jean-Christophe Léchenet, Enrico Tassi | 20m |
A tool called feqb synthesizes sound equality tests and correctness proofs for Coq inductive types used with the Mathematical Components library, handling very… | ||
| Compiling higher-order specifications to SMT solvers: how to deal with rejection ... | Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komandantskaya, Luca Arnaboldi | 27m |
Claims a verified pipeline that compiles higher-order Vehicle specifications to SMT while giving pinpointed rejections, implemented for Marabou-style backends… | ||
| FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores | Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy | 22m |
FastVer2 is a verified, concurrent monitor for the Faster key-value store: implemented in C (≈8,000 lines produced from ≈50,000 lines of F proofs) using the… | ||
| Formalising Decentralised Exchanges in Coq | Eske Hoy Nielsen, Danil Annenkov, Bas Spitters | 18m |
Claims a first formalisation in Coq of a decentralized exchange implementation (Dexter2) capturing cross-contract interactions, proves functional correctness… | ||
| Semantics of Probabilistic Programs using S-Finite Kernels in Coq | Reynald Affeldt, Cyril Cohen, Ayumu Saito | 24m |
Extends a Coq formalization of measure and integration by adding s-finite kernels to interpret typing judgments for a probabilistic language, and proves key… | ||
| Formalising Sharkovsky's Theorem (Proof Pearl) | Bhavik Mehta | 28m |
Formalisation of Sharkovsky's theorem and its converse appears in the Lean theorem prover, giving a machine-checked characterization of which minimal periods… | ||
| A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL | Katherine Kosaian, Yong Kiam Tan, André Platzer | 24m |
Formal verification of a first complete multivariate QE in Isabelle/HOL that hybridizes Ben-Or‑Kozen‑Reif and Tarski: it reduces quantifier elimination to sign… | ||
| P4Cub: A Little Language for Big Routers | Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parsia Ataei, Nate Foster | 18m |
P4Cub is an IR for P4 with a Petr4 front end and a claim of easier mechanized metatheory: it is mechanized in Coq with both large- and small-step semantics and… | ||
| ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER | Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy | 25m |
Claims a first formalization of ASN.1 DER with a mechanized proof of non-malleability and a verified compiler in F that uses the EverParse framework to produce… | ||
| Verifying term graph optimizations using Isabelle/HOL | Brae J. Webb, Ian J. Hayes, Mark Utting | 21m |
Formal verification of hundreds of GraalVM expression optimizations proceeds by extracting maximally shared subgraphs into terms and lifting term rewriting… | ||
| CompCert: a journey through the landscape of mechanized semantics for verified co... | Sandrine Blazy | 50m |
CompCert implements 18 verified compiler passes across 11 formally‑specified languages and proves semantics preservation by composable small-step semantics and… | ||
| Mechanised Semantics for Gated Static Single Assignment | Yann Herklotz, Delphine Demange, Sandrine Blazy | 22m |
Provides a formal, mechanised semantics for Gated Static Single Assignment mechanised in Coq and clarifies the role of gamma and eta gates with a… | ||
| Formalising the h-principle and sphere eversion | Patrick Massot, Floris van Doorn, Oliver Nash | 24m |
Formalisation in Lean of the local h‑principle for first‑order, open, ample partial differential relations proves Smale’s sphere eversion as a corollary, using… | ||
| A Formalized Reduction of Keller's Conjecture | Joshua Clune | 22m |
Formalization produces a machine-checked reduction from the infinite geometric statement of Keller’s conjecture to a finite graph problem, encodes… | ||
| Computing Cohomology Rings in Cubical Agda | Thomas Lamiaux, Axel Ljungström, Anders Mörtberg | 19m |
Claims a first fully mechanized, constructive definition of cohomology rings implemented in Cubical Agda, with concrete computations for spheres and the Klein… | ||
| CPP Business Meeting | Steve Zdancewic, Brigitte Pientka, Robbert Krebbers, Dmitriy Traytel | 25m |
Conference reports concrete numbers: 53 submissions, 25 accepted after a two‑month light double‑blind review with 33 PC members and about 20 external… | ||
| A Formalization of the Development Closedness Criterion for Left-Linear Term Rewr... | Christina Kohl, Aart Middeldorp | 23m |
Formalizes van Oostrom’s development closedness criterion for left-linear term rewrite systems by encoding multi-steps as proof terms and proving the diamond… | ||
| Formalizing and computing propositional quantifiers | Hugo Férée, Sam Van Gool | 22m |
Pitts’ 1992 result — propositional quantifiers definable inside intuitionistic propositional logic — is fully formalized in Coq formalization and an executable… | ||
| Encoding Dependently-Typed Constructions into Simple Type Theory | Anthony Bordg, Adrián Doña Mateo | 22m |
Claims an encoding of most of Lean’s dependent constructions into Isabelle/HOL by representing type families as a single set-valued function X : N → set, using… | ||
| A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive... | Yannick Forster, Felix Jahn, Gert Smolka | 19m |
Paper proves a constructive Cantor–Bernstein for enumerable discrete types and gives three explicit bijection constructions: a Myhill-style staged build with… | ||
| Aesop: White-Box Best-First Proof Search for Lean | Jannis Limperg, Asta Halkjær | 22m |
Aesop is a white-box proof-search tactic for Lean 4 that runs a tree search over user-registered rules and prioritises goals by best-first with per-rule… | ||
| A formalization of Doob's martingale convergence theorems in mathlib | Kexing Ying, Rémy Degenne | 22m |
Formalization of Doob’s martingale convergence theorems in mathlib proves almost-sure and L1 convergence for martingales, builds a conditional expectation via… | ||
| A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL | Angeliki Koutsoukou-Argyraki, Mantas Bakšys, Chelsea Edmonds | 20m |
The project formalises the Balog–Szemerédi–Gowers theorem in Isabelle/HOL, delivering the first proof assistant formalisation of that result, including a… | ||
| A Formal Disproof of Hirsch Conjecture | Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub | ? |
Claims a machine-checked counterexample to the Hirsch Conjecture: an explicit polytope whose graph diameter violates the Hirsch bound. Uses a formal proof… | ||
| Formalized Class Group Computations and Integral Points on Mordell Elliptic Curve... | Anne Baanen, Alex Best, Nirvana Coppola, Sander R. Dahmen | 22m |
Formalization proves integer solutions for several Mordell equations, notably y^2 = x^3 - 13 with x = 17, y = ±70, by formalizing ideal norms, quadratic rings… | ||
| nothing matches | ||