CPP 2022
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 2022 will be held on 17-18 January 2022 and will be co-located with POPL 2022 in Philadelphia, Pennsylvania, United States. The streamed talks of CPP 2022 are available on YouTube.
who it's for
formal verification researchers, Coq developers, Isabelle/HOL developers, verification engineers, theorem prover maintainers, programming language researchers, systems verification engineers
topics
Coq mechanization of metatheory; Isabelle/HOL transfer automation; Brzozowski-derivative lexer; CFML amortized data structures; Iris-based linearizability proofs; skeletal-semantics certified interpreter; certified string solving with automata; formal verification of microkernel IPC; verified seL4 proof engineering; verified Cairo program execution; formalised Lie algebras in Lean; forward build systems, formally
| title | author | length |
|---|---|---|
| A Drag-and-Drop Proof Tactic | Benjamin Werner, Pablo Donato, Pierre-Yves Strub | 13m |
A browser-playable prototype called Actima prototype implements drag-and-drop proof steps backed by deep inference and subformula linking, claiming… | ||
| A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem | Ariel E. Kellison | 23m |
States a direct constructive proof of the Steiner–Lehmus theorem that is fully machine-checked inside a constructive proof assistant, avoids the law of… | ||
| Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives | Derek Egolf, Sam Lasser, Kathleen Fisher | 19m |
Lexer based on Brzozowski derivatives moves from quadratic worst case to effectively linear time on a JSON benchmark by three verified refinements… | ||
| Specification and Verification of a Transient Stack | Alexandre Moine, Arthur Charguéraud, François Pottier | 14m |
Defines and machine-verified a scaled-down transient stack implemented as a list of fixed-capacity chunks with unique identifiers for ownership, copy‑on‑write… | ||
| Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr | Simon Friis Vindum, Lars Birkedal, Dan Frumin | 21m |
First formal specification and machine-checked proof of Meta Folly’s fine‑grained MPMC queue: an ML‑style implementation is shown to be a contextual refinement… | ||
| Applying Formal Verification to Microkernel IPC at Meta | Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli | 23m |
Project uses Iris in Coq to verify the microkernel IPC algorithms (not the full C), proving correctness of two queues verified implemented as non‑blocking… | ||
| Certified Abstract Machines for Skeletal Semantics | Guillaume Ambal, Serguei Lenglet, Alan Schmitt | 20m |
Automatic generation produces a certified OCaml interpreter from any language written in skeletal semantics by deriving two semantics: a relation-style… | ||
| CertiStr: A Certified String Solver | Shuanglong Kan, Anthony W. Lin, Philipp Ruemmer, Micha Schrader | 19m |
CertiStr is a certified solver for strings with concatenation and regular constraints, proven correct in Isabelle/HOL-certified OCaml extraction and… | ||
| An Extension of the Framework Types-To-Sets for Isabelle/HOL | Mihails Milehins | 23m |
An Isabelle/ HOL extension provides an interactive Isar framework that applies an extended relativization algorithm (ERA) to automatically convert type-based… | ||
| Semantic cut elimination for the logic of bunched implications, formalized in Coq | Dan Frumin | 24m |
Semantic proof of cut elimination for BI is formalized in Coq and gives a concrete model: closed sets of cut-free principal bunches (closure under arbitrary… | ||
| Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq | Mark Koch, Dominik Kirst | 24m |
The project mechanizes central metatheory of second‑order logic in Coq mechanization, producing about 8,000 lines of code (plus 1,500 reused) and… | ||
| Formalising Lie algebras | Oliver Nash | 20m |
Formalises finite‑dimensional Lie algebra theory in Lean + Mathlib, builds the classical families and the five exceptional algebras by constructing a free… | ||
| Implementing a category-theoretic framework for typed abstract syntax | Benedikt Ahrens, Ralph Matthes, Anders Mörtberg | 23m |
Mechanized extension of the UniMath/Coq framework produces simply‑typed syntax from signatures by generalizing signatures to non‑endofunctors, extending the… | ||
| (Deep) Induction Rules for GADTs | Patricia Johann, Enrico Ghiorzi | 24m |
Extends structural induction so it actually proves properties of many GADTs by deriving deep induction rules for non-truly-nested GADTs using an equal type and… | ||
| On homotopy of walks and spherical maps in homotopy type theory | Jonathan Prieto-Cubides | 18m |
Defines a decidable loop-reduction on directed multigraph walks and proves a normalization theorem: every walk reduces to a normal form that is walk-homotopic… | ||
| Windmills of the minds: an algorithm for Fermat's Two Squares Theorem | Hing Lun Chan | 20m |
Formalised in HOL, the method turns Ségier’s parity argument on involutions into a concrete loop: represent n = x^2 + 4yz as windmill patterns, alternate the… | ||
| A Compositional Proof Framework for FRETish Requirements | Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle | 22m |
Formalization defines a new denotational semantics for Fretish and proves semantic equivalence between Fretish requirements and the MTL formulas Fret… | ||
| Formally Verified Superblock Scheduling | Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino | 19m |
A certified scheduler that actually runs over superblocks is implemented and hooked into CompCert integration with a machine-checked semantic preservation… | ||
| Overcoming Restraint: Composing Verification of Foreign Functions with Cogent | Louis Cheung, Liam OConnor, Christine Rizkallah | 17m |
Cogent’s FFI is proven to preserve uniqueness typing and memory safety while composing Cogent proofs down to C: the compiler’s multi‑phase refinement pipeline… | ||
| Reflection, Rewinding, and Coin-Toss in EasyCrypt | Denis Firsov, Dominique Unruh | 15m |
Derives a concrete library of lemmas that reflect EasyCrypt procedures into explicit distributions d_a over final module states and shows composition via… | ||
| Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting | Michael Färber | 22m |
Reimplements a Dedukti-like kernel for the lambda-Pi calculus modulo rewriting in Rust and builds a small, memory- and thread-safe proof checker called… | ||
| A verified algebraic representation of Cairo program execution | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman | 26m |
Formal proof that the algebraic encoding used to generate real STARK certificates implies an actual Cairo execution: the project formalizes the Cairo machine… | ||
| Formal Verification of a Distributed Dynamic Reconfiguration Protocol | William Schultz, Ian Dardik, Stavros Tripakis | 24m |
Formal, machine-checked TLA+ proofs establish safety of MongoRaftReconfig: an inductive invariant of 20 conjuncts and a TLAPS proof of LeaderCompleteness and… | ||
| Forward build systems, formally | Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt | 22m |
Defines forward-build correctness as: either reproduce the result of running the script sequentially or report a hazard. Models commands, filesystems… | ||
| Structural Embeddings Revisited | Cesar Munoz | 57m |
Formal verification shows the parallel-landing alert algorithm issues warnings for conflicts that occur between 9.5–10 seconds (a counterexample appears at… | ||
| Coq's vibrant ecosystem for verification engineering | Andrew W. Appel | 01h 04m |
Coq now supports end-to-end, layered verification: a Verified Software Toolchain connects C proofs to the CompCert semantics and backends like CompCert and… | ||
| The seL4 verification: the art and craft of proof and the reality of commercial s | June Andronick | 01h 07m |
A formally verified seL4 microkernel exists end-to-end: a C implementation of roughly 500 functions (10–15k LOC originally) is proved correct against an… | ||
| nothing matches | ||