| 2023 | Real-Time Double-Ended Queue Verified (Proof Pearl). | Balzs Tth, Tobias Nipkow |
| 2023 | A Sound and Complete Projection for Global Types. | Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone |
| 2023 | POSIX Lexing with Bitcoded Derivatives. | Chengsong Tan, Christian Urban |
| 2023 | Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. | Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, Talia Ringer |
| 2023 | Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. | Pierre Pomeret-Coquot, Hlne Fargier, rik Martin-Dorel |
| 2023 | An Extensible User Interface for Lean 4. | Wojciech Nawrocki, Edward W. Ayers, Gabriel Ebner |
| 2023 | A Formalisation of Gallagher's Ergodic Theorem. | Oliver Nash |
| 2023 | Group Cohomology in the Lean Community Library. | Amelia Livingston |
| 2023 | Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. | Dominique Larchey-Wendling, Jean-Franois Monin |
| 2023 | Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). | Robbert Krebbers |
| 2023 | Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). | Angeliki Koutsoukou-Argyraki |
| 2023 | Formalizing Almost Development Closed Critical Pairs (Short Paper). | Christina Kohl, Aart Middeldorp |
| 2023 | Constructive Final Semantics of Finite Bags. | Philipp Joram, Niccol Veltri |
| 2023 | MizAR 60 for Mizar 50. | Jan Jakubuv, Karel Chvalovsk, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsk, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban |
| 2023 | Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. | Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato |
| 2023 | LISA - A Modern Proof System. | Simon Guilloud, Sankalp Gambhir, Viktor Kuncak |
| 2023 | Implementing More Explicit Definitional Expansions in Mizar (Short Paper). | Adam Grabowski, Artur Kornilowicz |
| 2023 | Formalizing Norm Extensions and Applications to Number Theory. | Mara Ins de Frutos-Fernndez |
| 2023 | Formalising Yoneda Ext in Univalent Foundations. | Jarl G. Taxers Flaten |
| 2023 | Closure Properties of General Grammars - Formally Verified. | Martin Dvorak, Jasmin Blanchette |
| 2023 | Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. | Lawrence Dunn, Val Tannen, Steve Zdancewic |
| 2023 | Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. | Lus Cruz-Filipe, Fabrizio Montesi |
| 2023 | Automated Theorem Proving for Metamath. | Mario Carneiro, Chad E. Brown, Josef Urban |
| 2023 | Reimplementing Mizar in Rust. | Mario Carneiro |
| 2023 | No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. | Roger Bosman, Georgios Karachalias, Tom Schrijvers |