CPP 2026
27 papers
- A Certifying Proof Assistant for Synthetic Mathematics in Lean
- A Lambda-Superposition Tactic for Isabelle/HOL
- A Recipe for Modular Verification of Generic Tree Traversals
- A Rose Tree Is Blooming (Proof Pearl)
- Adding Sorts to an Isabelle Formalization of Superposition
- Adhesive Category Theory for Graph Rewriting in Rocq
- Bar Inductive Predicates for Constructive Algebra in Rocq
- Brack: A Verified Compiler for Scheme via CakeML
- Building Blocks for Step-Indexed Program Logics
- Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda
- Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
- Certifying the Decidability of the Word Problem in Monoids at Large
- Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
- Cylindrical Algebraic Decomposition in Coq/Rocq
- Enhancing Symbolic Execution with Machine-Checked Safety Proofs
- Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
- Formalizing Polynomial Laws and the Universal Divided Power Algebra
- Foundational Verification of Running-Time Bounds for Interactive Programs
- Higher Order Differential Calculus in Mathlib
- Layers of Confluence for Actors
- Mechanized Dominator Tree Certification
- Mechanizing Synthetic Tait Computability in Istari
- Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
- Precise Reasoning about Container-Internal Pointers with Logical Pinning
- Towards Composable Proofs of Cache Coherence Protocols
- Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
- Verified VCG and Verified Compiler for Dafny