CPP 2023
27 papers
- A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- A Formal Disproof of Hirsch Conjecture
- A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL
- A Formalization of Doob's Martingale Convergence Theorems in mathlib
- A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
- A Formalized Reduction of Keller's Conjecture
- ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
- Aesop: White-Box Best-First Proof Search for Lean
- CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)
- Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
- Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
- Computing Cohomology Rings in Cubical Agda
- Encoding Dependently-Typed Constructions into Simple Type Theory
- FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
- Formalising Decentralised Exchanges in Coq
- Formalising Sharkovsky's Theorem (Proof Pearl)
- Formalising the h-Principle and Sphere Eversion
- Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
- Formalizing and Computing Propositional Quantifiers
- Improved Assistance for Interactive Proof (Keynote)
- Mechanised Semantics for Gated Static Single Assignment
- P4Cub: A Little Language for Big Routers
- Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi
- Semantics of Probabilistic Programs using s-Finite Kernels in Coq
- Terms for Efficient Proof Checking and Parsing
- Verifying Term Graph Optimizations using Isabelle/HOL