| 2023 | 14th International Conference on Interactive Theorem Proving, ITP 2023, Białystok, Poland, July 31 - August 4, 2023 Adam Naumowicz, René Thiemann |
| 2023 | A Formal Analysis of RANKING. Mohammad Abdulaziz, Christoph Madlener |
| 2023 | A Formalisation of Gallagher's Ergodic Theorem. Oliver Nash |
| 2023 | A Proof-Producing Compiler for Blockchain Applications. Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
| 2023 | A Sound and Complete Projection for Global Types. Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone |
| 2023 | An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. David Kurniadi Angdinata, Junyan Xu |
| 2023 | An Extensible User Interface for Lean 4. Wojciech Nawrocki, Edward W. Ayers, Gabriel Ebner |
| 2023 | Automated Theorem Proving for Metamath. Mario Carneiro, Chad E. Brown, Josef Urban |
| 2023 | Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel |
| 2023 | Certifying Higher-Order Polynomial Interpretations. Niels van der Weide, Deivid Vale, Cynthia Kop |
| 2023 | Closure Properties of General Grammars - Formally Verified. Martin Dvorak, Jasmin Blanchette |
| 2023 | Constructive Final Semantics of Finite Bags. Philipp Joram, Niccolò Veltri |
| 2023 | Dependently Sorted Theorem Proving for Mathematical Foundations. Yiming Xu, Michael Norrish |
| 2023 | Fast, Verified Computation for Candle. Oskar Abrahamsson, Magnus O. Myreen |
| 2023 | Fermat's Last Theorem for Regular Primes (Short Paper). Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi |
| 2023 | Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). Angeliki Koutsoukou-Argyraki |
| 2023 | Formalising Yoneda Ext in Univalent Foundations. Jarl G. Taxerås Flaten |
| 2023 | Formalising the Proj Construction in Lean. Jujian Zhang |
| 2023 | Formalizing Almost Development Closed Critical Pairs (Short Paper). Christina Kohl, Aart Middeldorp |
| 2023 | Formalizing Functions as Processes. Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen |
| 2023 | Formalizing Norm Extensions and Applications to Number Theory. María Inés de Frutos-Fernández |
| 2023 | Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). Akihisa Yamada, Jérémy Dubut |
| 2023 | Foundational Verification of Stateful P4 Packet Processing. Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel |
| 2023 | Front Matter, Table of Contents, Preface, Conference Organization. |
| 2023 | Group Cohomology in the Lean Community Library. Amelia Livingston |
| 2023 | Implementing More Explicit Definitional Expansions in Mizar (Short Paper). Adam Grabowski, Artur Kornilowicz |
| 2023 | Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). Robbert Krebbers |
| 2023 | LISA - A Modern Proof System. Simon Guilloud, Sankalp Gambhir, Viktor Kuncak |
| 2023 | Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann |
| 2023 | MizAR 60 for Mizar 50. Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban |
| 2023 | No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. Roger Bosman, Georgios Karachalias, Tom Schrijvers |
| 2023 | Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. Luís Cruz-Filipe, Fabrizio Montesi |
| 2023 | POSIX Lexing with Bitcoded Derivatives. Chengsong Tan, Christian Urban |
| 2023 | Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. Dominique Larchey-Wendling, Jean-François Monin |
| 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 | Real-Time Double-Ended Queue Verified (Proof Pearl). Balázs Tóth, Tobias Nipkow |
| 2023 | Reimplementing Mizar in Rust. Mario Carneiro |
| 2023 | Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato |
| 2023 | Slice Nondeterminism. Niels F. W. Voorneveld |
| 2023 | Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. Lawrence Dunn, Val Tannen, Steve Zdancewic |