| 2023 | Formalising Sharkovsky's Theorem (Proof Pearl). | Bhavik Mehta |
| 2023 | Aesop: White-Box Best-First Proof Search for Lean. | Jannis Limperg, Asta Halkjr From |
| 2023 | Computing Cohomology Rings in Cubical Agda. | Thomas Lamiaux, Axel Ljungstrm, Anders Mrtberg |
| 2023 | A Formalisation of the Balog-Szemerdi-Gowers Theorem in Isabelle/HOL. | Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds |
| 2023 | A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. | Katherine Kosaian, Yong Kiam Tan, Andr Platzer |
| 2023 | A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. | Christina Kohl, Aart Middeldorp |
| 2023 | Improved Assistance for Interactive Proof (Keynote). | Cezary Kaliszyk |
| 2023 | Mechanised Semantics for Gated Static Single Assignment. | Yann Herklotz, Delphine Demange, Sandrine Blazy |
| 2023 | Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. | Benjamin Grgoire, Jean-Christophe Lchenet, Enrico Tassi |
| 2023 | Formalizing and Computing Propositional Quantifiers. | Hugo Fre, Sam van Gool |
| 2023 | Terms for Efficient Proof Checking and Parsing. | Michael Frber |
| 2023 | Formalising the h-Principle and Sphere Eversion. | Floris van Doorn, Patrick Massot, Oliver Nash |
| 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 | A Formalized Reduction of Keller's Conjecture. | Joshua Clune |
| 2023 | Encoding Dependently-Typed Constructions into Simple Type Theory. | Anthony Bordg, Adrin Doa Mateo |
| 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 | CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). | Sandrine Blazy |
| 2023 | Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. | Anne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen |
| 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 | A Formal Disproof of Hirsch Conjecture. | Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub |
| 2023 | Semantics of Probabilistic Programs using s-Finite Kernels in Coq. | Reynald Affeldt, Cyril Cohen, Ayumu Saito |
| 2023 | A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). | Yannick Forster, Felix Jahn, Gert Smolka |
| 2022 | Mechanized verification of a fine-grained concurrent queue from meta's folly library. | Simon Friis Vindum, Dan Frumin, Lars Birkedal |
| 2022 | Forward build systems, formally. | Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt |
| 2022 | Formally verified superblock scheduling. | Cyril Six, Lo Gourdin, Sylvain Boulm, David Monniaux, Justus Fasse, Nicolas Nardino |