| 2024 | 15th International Conference on Interactive Theorem Proving, ITP 2024, Tbilisi, Georgia, September 9-14, 2024 Yves Bertot, Temur Kutsia, Michael Norrish |
| 2024 | A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. Reynald Affeldt, Zachary Stone |
| 2024 | A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. Sewon Park, Holger Thies |
| 2024 | A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows. Mohammad Abdulaziz, Thomas Ammer |
| 2024 | A Formal Proof of R(4, 5)=25. Thibault Gauthier, Chad E. Brown |
| 2024 | A Formalization of the General Theory of Quaternions. Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, Mauricio Ayala-Rincón |
| 2024 | A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL. Michikazu Hirata |
| 2024 | A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. Vincent Jackson, Toby Murray, Christine Rizkallah |
| 2024 | A Modular Formalization of Superposition in Isabelle/HOL. Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret |
| 2024 | A Verified Earley Parser. Martin Rau, Tobias Nipkow |
| 2024 | Abstractions for Multi-Sorted Substitutions. Hannes Saffrich |
| 2024 | Alpha-Beta Pruning Verified (Invited Talk). Tobias Nipkow |
| 2024 | An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility. Dohan Kim |
| 2024 | An Operational Semantics in Isabelle/HOL-CSP. Benoît Ballenghien, Burkhart Wolff |
| 2024 | Completeness of Asynchronous Session Tree Subtyping in Coq. Burak Ekici, Nobuko Yoshida |
| 2024 | Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. Karol Pak, Cezary Kaliszyk |
| 2024 | Correctly Compiling Proofs About Programs Without Proving Compilers Correct. Audrey Seo, Christopher Lam, Dan Grossman, Talia Ringer |
| 2024 | Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. Andrew Tolmach, Chris Chhak, Sean Noble Anderson |
| 2024 | Distributed Parallel Build for the Isabelle Archive of Formal Proofs. Fabian Huch, Makarius Wenzel |
| 2024 | Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad |
| 2024 | End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond |
| 2024 | Formal Verification of the Empty Hexagon Number. Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule |
| 2024 | Formalising Half of a Graduate Textbook on Number Theory (Short Paper). Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li |
| 2024 | Formalizing the Algebraic Small Object Argument in UniMath. Dennis Hilhorst, Paige Randall North |
| 2024 | Formalizing the Cholesky Factorization Theorem. Carl Kwan, Warren A. Hunt Jr. |
| 2024 | Front Matter, Table of Contents, Preface, Conference Organization. |
| 2024 | Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). Sam Ezeh |
| 2024 | Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. Floris van Doorn, Heather Macbeth |
| 2024 | Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge. Kai Obendrauf, Anne Baanen, Patrick Koopmann, Vera Stebletsova |
| 2024 | Mechanized HOL Reasoning in Set Theory. Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kuncak |
| 2024 | Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. Marc Hermes, Robbert Krebbers |
| 2024 | Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics. Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani |
| 2024 | Robust Mean Estimation by All Means (Short Paper). Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann |
| 2024 | Taming Differentiable Logics with Coq Formalisation. Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark |
| 2024 | Teaching Mathematics Using Lean and Controlled Natural Language. Patrick Massot |
| 2024 | The Directed Van Kampen Theorem in Lean. Henning Basold, Peter Bruin, Dominique Lawson |
| 2024 | The Functor of Points Approach to Schemes in Cubical Agda. Max Zeuner, Matthias Hutzler |
| 2024 | The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter |
| 2024 | Towards Solid Abelian Groups: A Formal Proof of Nöbeling's Theorem. Dagur Asgeirsson |
| 2024 | Translating Libraries of Definitions and Theorems Between Proof Systems (Invited Talk). Frédéric Blanqui |
| 2024 | Typed Compositional Quantum Computation with Lenses. Jacques Garrigue, Takafumi Saikawa |
| 2024 | Verifying Peephole Rewriting in SSA Compiler IRs. Siddharth Bhat, Alex C. Keizer, Chris Hughes, Andrés Goens, Tobias Grosser |
| 2024 | Verifying Software Emulation of an Unsupported Hardware Instruction. Samuel Gruetter, Thomas Bourgeat, Adam Chlipala |