September 9–14, 2024
Fifteenth Conference on Interactive Theorem Proving
Tbilisi, Georgia, 2024
Invited Speakers
- Frédéric Blanqui (INRIA), Translating libraries of definitions and theorems between proof systems
- Tobias Nipkow (Technical University of Munich), Alpha Beta Pruning Verified
Tutorial
- Evgenia Karunus, Visualising Mathematical Proof: Paperproof
Proceedings
The proceedings of the conference is available online.
Program Schedule
The main conference room is the Room 115 (1st floor). Location of coffee breaks, school and workshops will be announced during the conference.
Monday, 9 September 2024
| 09:00-09:30 | Registration |
| Session 1: Invited Talk. Chair: Yves Bertot | |
| 09:30-10:30 | Tobias Nipkow: Alpha Beta Pruning Verified |
| 10:30-11:00 | Coffee Break |
| Session 2. Chair: Temur Kutsia | |
| 11:00-11:30 | Andrew Tolmach, Chris Chhak, and Sean Anderson: Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model (slides) |
| 11:30-12:00 | Audrey Seo, Christopher Lam, Dan Grossman, and Talia Ringer: Correctly Compiling Proofs About Programs Without Proving Compilers Correct |
| 12:00-12:30 | Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser: Verifying Peephole Rewriting In SSA Compiler Irs |
| 12:30-14:00 | Lunch |
| Session 3. Chair: Mauricio Ayala-Rincón | |
| 14:00-14:30 | Hannes Saffrich: Abstractions for Multi-Sorted Substitutions |
| 14:30-15:00 | Benoît Ballenghien and Burkhart Wolff: An Operational Semantics in Isabelle/HOL-CSP |
| 15:00-15:30 | Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, and Kathrin Stark: Taming Differentiable Logics with Coq Formalisation |
| 15:30-16:00 | Coffee Break |
| Session 4. Chair: Mario Carneiro | |
| 16:00-16:30 | Martin Rau and Tobias Nipkow: A Verified Earley Parser |
| 16:30-17:00 | Henning Basold, Peter Bruin, and Dominique Lawson: The Directed Van Kampen Theorem in Lean |
| 17:00-17:15 | Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, and Carsten Schürmann: Robust Mean Estimation by All Means (short paper) |
| 18:00-22:00 | Welcome Dinner |
Tuesday, 10 September 2024
| Session 5. Chair: Manuel Eberl | |
| 09:00-09:30 | Jacques Garrigue and Takafumi Saikawa: Typed compositional quantum computation with lenses |
| 09:30-10:00 | Karol Pąk and Cezary Kaliszyk: Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers |
| 10:00-10:30 | Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón: A Formalization of the General Theory of Quaternions |
| 10:30-11:00 | Coffee Break |
| Session 6. Chair: Mauricio Ayala-Rincón | |
| 11:00-11:30 | Mohammad Abdulaziz and Thomas Ammer: A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows |
| 11:30-12:00 | Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter: The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant |
| 12:00-12:30 | Mallku Soldevila, Rodrigo Ribeiro, and Beta Ziliani: Redex2Coq: Towards a Theory of Decidability of Redex’s Reduction Semantics (video) |
| 12:30-14:00 | Lunch |
| Session 7. Chair: Burkhart Wolff | |
| 14:00-14:30 | Vincent Jackson, Toby Murray, and Christine Rizkallah: A Generalised Union of Rely–Guarantee and Separation Logic using Permission Algebras |
| 14:30-15:00 | Marc Hermes and Robbert Krebbers: Modular Verification of Intrusive List and Tree Data Structures in Separation Logic |
| 15:00-15:30 | Samuel Gruetter, Thomas Bourgeat, and Adam Chlipala: Verifying Software Emulation of an Unsupported Hardware Instruction |
| 15:30-16:00 | Coffee Break |
| Session 8. Chair: Floris van Doorn | |
| 16:00-16:30 | Thibault Gauthier and Chad E. Brown: A Formal Proof of R(4,5)=25 |
| 16:30-17:00 | Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule: Formal Verification of the Empty Hexagon Number |
Wednesday, 11 September 2024
| 09:00-22:00 | Excursion and Dinner |
Thursday, 12 September 2024
Friday, 13 September 2024
Saturday, 14 September 2024
| 09:00-10:30 | Evgenia Karunus, Visualising Mathematical Proof: Paperproof | Isabelle Workshop | Coq Workshop |
| 10:30-11:00 | Coffee Break | ||
| 11:00-12:30 | School on Logic and Language | Isabelle Workshop | Coq Workshop |
| 12:30-14:00 | Lunch | ||
| 14:00-15:30 | School on Logic and Language | Isabelle Workshop | Coq Workshop |
| 15:30-16:00 | Coffee Break | ||
| 16:00-18:00 | School on Logic and Language | Isabelle Workshop | Coq Workshop |
Sunday, 15 September 2024
| 08:30-22:00 | Excursion and Dinner only for School and Workshop participants |
List of Accepted Papers
- Mohammad Abdulaziz and Thomas Ammer, A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows
- Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa and Carsten Schürmann, Robust mean estimation by all means (short paper)
- Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz and Kathrin Stark, Taming Differentiable Logics With Coq Formalisation
- Reynald Affeldt and Zachary Stone, A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
- Dagur Asgeirsson, Towards solid abelian groups: A formal proof of Nöbeling's theorem
- Benoît Ballenghien and Burkhart Wolff, An Operational Semantics in Isabelle/HOL-CSP
- Henning Basold, Peter Bruin and Dominique Lawson, The Directed Van Kampen Theorem in Lean
- Siddharth Bhat, Alex Keizer, Chris Hughes, Andres Goens and Tobias Grosser, Verifying Peephole Rewriting In SSA Compiler IRs
- Joshua Clune, Yicheng Qian, Alexander Bentkamp and Jeremy Avigad, Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory
- Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro and Mauricio Ayala-Rincón, A Formalization of the General Theory of Quaternions
- Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette and Sophie Tourret, A Modular Formalization of Superposition in Isabelle/HOL
- Manuel Eberl, Anthony Bordg, Lawrence Paulson and Wenda Li, Formalising Half of a Graduate Textbook on Number Theory
- Burak Ekici and Nobuko Yoshida, Completeness of Asynchronous Session Tree Subtyping in Coq
- Sam Ezeh, Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4 (Short paper)
- Florian Faissole, Paul Geneau de Lamarlière and Guillaume Melquiond, End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation
- Jacques Garrigue and Takafumi Saikawa, Typed compositional quantum computation with lenses
- Thibault Gauthier and Chad Brown, A Formal Proof of R(4,5) = 25
- Samuel Gruetter, Thomas Bourgeat and Adam Chlipala, Verifying Software Emulation of an Unsupported Hardware Instruction
- Simon Guilloud, Sankalp Gambhir, Andrea Gilot and Viktor Kuncak, Mechanized Embedding of HOL in Set Theory
- Marc Hermes and Robbert Krebbers, Modular Verification of Intrusive List and Tree Data Structures in Separation Logic
- Dennis Hilhorst and Paige North, Formalizing the algebraic small object argument in UniMath
- Michikazu Hirata, A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL
- Fabian Huch and Makarius Wenzel, Distributed Parallel Build for the Isabelle Archive of Formal Proofs
- Vincent Jackson, Toby Murray and Christine Rizkallah, A Generalised Union of Rely-Guarantee and Separation Logic using Permission Algebras
- Dohan Kim, An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility
- Carl Kwan and Warren Hunt, Formalizing the Cholesky Factorization Theorem
- Yann Leray, Gaëtan Gilbert, Nicolas Tabareau and Théo Winterhalter, The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant
- Patrick Massot, Teaching mathematics using Lean and controlled natural language
- Kai Obendrauf, Anne Baanen, Patrick Koopmann and Vera Stebletsova, Lean Formalization of a Completeness Proof for Coalition Logic with Common Knowledge
- Karol Pąk and Cezary Kaliszyk, Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
- Sewon Park and Holger Thies, A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations
- Martin Rau and Tobias Nipkow, A Verified Earley Parser
- Hannes Saffrich, Abstractions for Multi-Sorted Substitutions
- Audrey Seo, Christopher Lam, Dan Grossman and Talia Ringer, Correctly Compiling Proofs About Programs Without Proving Compilers Correct
- Mallku Soldevila, Rodrigo Ribeiro and Beta Ziliani, Redex2Coq: towards a theory of decidability of Redex’s reduction semantics
- Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro and Marijn Heule, Formal Verification of the Empty Hexagon Number
- Andrew Tolmach, Chris Chhak and Sean Anderson, Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model
- Floris van Doorn and Heather Macbeth, Integrals within integrals: a formalization of the Gagliardo-Nirenberg-Sobolev inequality
- Max Zeuner and Matthias Hutzler, The Functor of Points Approach to Schemes in Cubical Agda