| 2023 | A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). Yannick Forster, Felix Jahn, Gert Smolka |
| 2023 | A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. Katherine Kosaian, Yong Kiam Tan, André Platzer |
| 2023 | A Formal Disproof of Hirsch Conjecture. Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub |
| 2023 | A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds |
| 2023 | A Formalization of Doob's Martingale Convergence Theorems in mathlib. Kexing Ying, Rémy Degenne |
| 2023 | A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. Christina Kohl, Aart Middeldorp |
| 2023 | A Formalized Reduction of Keller's Conjecture. Joshua Clune |
| 2023 | ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy |
| 2023 | Aesop: White-Box Best-First Proof Search for Lean. Jannis Limperg, Asta Halkjær From |
| 2023 | CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). Sandrine Blazy |
| 2023 | Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi |
| 2023 | 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 |
| 2023 | Computing Cohomology Rings in Cubical Agda. Thomas Lamiaux, Axel Ljungström, Anders Mörtberg |
| 2023 | Encoding Dependently-Typed Constructions into Simple Type Theory. Anthony Bordg, Adrián Doña Mateo |
| 2023 | 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 |
| 2023 | Formalising Decentralised Exchanges in Coq. Eske Hoy Nielsen, Danil Annenkov, Bas Spitters |
| 2023 | Formalising Sharkovsky's Theorem (Proof Pearl). Bhavik Mehta |
| 2023 | Formalising the h-Principle and Sphere Eversion. Floris van Doorn, Patrick Massot, Oliver Nash |
| 2023 | Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. Anne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen |
| 2023 | Formalizing and Computing Propositional Quantifiers. Hugo Férée, Sam van Gool |
| 2023 | Improved Assistance for Interactive Proof (Keynote). Cezary Kaliszyk |
| 2023 | Mechanised Semantics for Gated Static Single Assignment. Yann Herklotz, Delphine Demange, Sandrine Blazy |
| 2023 | P4Cub: A Little Language for Big Routers. Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster |
| 2023 | Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi |
| 2023 | Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023 Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic |
| 2023 | Semantics of Probabilistic Programs using s-Finite Kernels in Coq. Reynald Affeldt, Cyril Cohen, Ayumu Saito |
| 2023 | Terms for Efficient Proof Checking and Parsing. Michael Färber |
| 2023 | Verifying Term Graph Optimizations using Isabelle/HOL. Brae J. Webb, Ian J. Hayes, Mark Utting |