26-29 July, 2026
Seventeenth Conference on Interactive Theorem Proving
Lisbon, Portugal, 2026
, by Deensel, under Creative Commons license.
, by Ввласенко, under Creative Commons license.
, by Alvesgaspar, under Creative Commons license.
, by Ingo Mehling, under Creative Commons license.
Invited Speakers
Dominic Mulligan, Amazon Web Services
Dominique Unruh, RWTH Aachen and University of Tartu
Program Schedule
Sunday, 26th July 2026
| 09:00-10:00 | FLOC Keynote: Leonardo de Moura |
| 10:00-11:00 | Coffee Break |
| Session 1: Formalisation of Mathematics 11:00 - 12:00 | |
| 11:00-11:30 | Dominique Unruh: Complex Bounded Operators in Isabelle/HOL |
| 11:30-12:00 | Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda: Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral |
| 12:00-14:00 | Lunch |
| Session 2: Formalisation of Algorithms 14:00 - 15:30 | |
| 14:00-14:30 | Ricardo Almeida, Blair Archibald, Basile Pesin, Michele Sevegnani: Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations |
| 14:30-15:00 | Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Tomás Vallejos Parada: Functional Correctness of an Optimized Modular Inversion Algorithm |
| 15:00-15:30 | Makoto Kanazawa: Verification of the Garsia–Wachs Algorithm |
| 15:30-16:30 | Coffee Break |
| Session 3: Program Logics 16:30 - 17:50 | |
| 16:30-17:00 | Peter Lammich: Fractional Separation Logic in Isabelle/LLVM |
| 17:00-17:30 | Valentin Mikhalchuk, Vladimir Gladshtein, Ilya Sergey: Lazy Proof Automation for Separation Logic |
| 17:30-18:00 | Luís Cruz-Filipe, Thomas Wulff Heissel: Formalizing a Hoare Calculus for Choreographic Programming |
| 18:00-20:00 | Reception |
Monday, 27th July 2026
| 09:00-10:00 | ITP Invited Talk: Dominic Mulligan |
| 10:00-11:00 | Coffee Break |
| Session 4: Verification and Model Checking 11:00 - 12:00 | |
| 11:00-11:30 | Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, Burkhart Wolff: Automated Verification of Robot Software Models with Assume–Guarantee Reasoning in Isabelle/HOL |
| 11:30-12:00 | Oliver Emil Bøving, Christoph Matheja: Securing the Foundations of an Intermediate Language for Probabilistic Program Verification |
| 12:00-14:00 | Lunch |
| Session 5: AI and ITP 14:00 - 15:30 | |
| 14:00-14:30 | Amitayush Thakur, George Tsoukalas, Greg Durrett, Swarat Chaudhuri: ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving |
| 14:30-15:00 | Zeke Medley, Panagiotis Manolios: Feedback & Synthesis in LLM-Assisted Termination Proofs |
| 15:00-15:30 | Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck: LeanArchitect: Automating Blueprint Generation for Humans and AI |
| 15:30-16:30 | Coffee Break |
| Session 6: Formalisation of Mathematics & AI 16:30 - 18:00 | |
| 16:30-17:00 | Eric Jonathan Wang, Elif Uskuplu: Formalizing the Bruck–Ryser–Chowla Theorem: Combinatorial Design Theory in Lean |
| 17:00-17:20 | Cameron Freer: Three Roads to de Finetti's Theorem in Lean (Short Paper) |
| 17:20-17:40 | Thomas Ammer, Mohammad Abdulaziz, Christoph Madlener: Formal Primal-Dual Algorithm Analysis (Short Paper) |
| 17:40-18:00 | Josef Urban: 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper) |
| 18:00-19:00 | Business Meeting: AI and ITP Conference Series |
| 19:00-20:00 | AI for Math Happy Hour ("Differentiated" Networking) |
Tuesday, 28th July 2026
| 09:00-10:00 | FLOC Keynote: Işıl Dillig |
| 10:00-11:00 | Coffee Break |
| Session 7: Proof Theory and Types 11:00 - 12:00 | |
| 11:00-11:30 | Yiming Lin, Ian Kariniemi, Yao Li: Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees |
| 11:30-12:00 | Meven Lennon-Bertrand, Alexis Saurin: Bidirectional Interpolation for the Lambda-Calculus – Revisiting and Formalising Craig–Čubrić Interpolation |
| 12:00-14:00 | Lunch |
| Session 8: User Interfaces and Compilers 14:00 - 15:30 | |
| 14:00-14:30 | Maria Khakimova, Sára Juhošová, Jaro Reinders, Jesper Cockx: Enhancing Interactive Theorem Prover Error Messages with Hints |
| 14:30-15:00 | Vladimir Gladshtein, K. Rustan M. Leino: Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language |
| 15:00-15:30 | Reed Mullanix, Jacques Carette: Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages |
| 15:30-16:30 | Coffee Break |
| Session 9: Automation and Tactics 16:30 - 18:00 | |
| 16:30-16:50 | Arend Mellendijk: A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper) |
| 16:50-17:10 | Jonas Bodingbauer, Marton Hajdu, Laura Kovacs, Axel Polaczek, Michael Rawson: Lean on Vampire Proofs (Short Paper) |
| 17:10-17:40 | Johann Rosain, Julie Cailler: TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq |
| 17:40-18:00 | Aeacus Sheng, Wenda Li and Paul JacksonFaster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper) |
| 19:00-23:00 | Banquet |
Wednesday, 29th July 2026
| 09:00-10:00 | ITP Invited Talk: Dominique Unruh |
| 10:00-11:00 | Coffee Break |
| Session 10: Automata and Coinduction 11:00 - 12:00 | |
| 11:00-11:30 | Arthur Correnson, Iona Kuhn, Bernd Finkbeiner: Completing Almost Fair Simulations |
| 11:30-12:00 | Jamie Wright, Liron Cohen, Reuben N. S. Rowe, Andrei Popescu: Certified Infinite Descent Criteria in Isabelle/HOL |
| 12:00-14:00 | Lunch |
| Session 11: Formalisation of Mathematics-3 14:00 - 15:30 | |
| 14:00-14:30 | Garett Cunningham, Daniel Zach, Stefan Friedl: Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean |
| 14:30-15:00 | Manuel Eberl, Wenda Li, Lawrence C. Paulson: From Weierstraß to Dedekind: Formalising Foundations of Modular Forms |
| 15:00-15:30 | James Gallicchio, Cayden Codel, Jeremy Avigad, Marijn J. H. Heule: An End-to-End Verification of Keller's Conjecture |
| 15:30-16:30 | Coffee Break |
| Session 12 16:30 - 18:00 | |
| 16:30-17:00 | Omer Keskin, Nobuko Yoshida, Rob van Glabbeek: Formally Verified Liveness with Multiparty Session Types in Rocq |
| 17:00-17:30 | Sage Binder, Hanna Lachnitt, Katherine Kosaian: Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar |
| 17:30-18:00 | Damien Pous: String Diagrams for Monoidal Categories, in Rocq |
List of Accepted Papers
- Ricardo Almeida, Blair Archibald, Basile Pesin and Michele Sevegnani. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations
- Thomas Ammer, Mohammad Abdulaziz and Christoph Madlener. Formal Primal-Dual Algorithm Analysis (Short Paper)
- Sage Binder, Hanna Lachnitt and Katherine Kosaian. Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
- Jonas Bodingbauer, Marton Hajdu, Laura Kovacs, Axel Polaczek and Michael Rawson. Lean on Vampire Proofs (Short Paper)
- Oliver Emil Bøving and Christoph Matheja. Securing the Foundations of an Intermediate Language for Probabilistic Program Verification
- Arthur Correnson, Iona Kuhn and Bernd Finkbeiner. Completing Almost Fair Simulations
- Luís Cruz-Filipe and Thomas Wulff Heissel. Formalizing a Hoare Calculus for Choreographic Programming
- Garett Cunningham, Daniel Zach and Stefan Friedl. Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean
- Manuel Eberl, Wenda Li and Lawrence C. Paulson. From Weierstraß to Dedekind: Formalising Foundations of Modular Forms
- Cameron Freer. Three Roads to de Finetti's Theorem in Lean: Short Paper
- James Gallicchio, Cayden Codel, Jeremy Avigad and Marijn J. H. Heule. An End-to-End Verification of Keller's Conjecture
- Vladimir Gladshtein and K. Rustan M. Leino. Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language
- Makoto Kanazawa. Verification of the Garsia–Wachs Algorithm
- Omer Keskin, Nobuko Yoshida and Rob van Glabbeek. Formally Verified Liveness with Multiparty Session Types in Rocq
- Maria Khakimova, Sára Juhošová, Jaro Reinders and Jesper Cockx. Enhancing Interactive Theorem Prover Error Messages with Hints
- Peter Lammich. Fractional Separation Logic in Isabelle/LLVM
- Meven Lennon-Bertrand and Alexis Saurin. Bidirectional Interpolation for the Lambda-Calculus – Revisiting and Formalising Craig-Čubrić Interpolation
- Yiming Lin, Ian Kariniemi and Yao Li . Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees
- Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub and Tomás Vallejos Parada. Functional correctness of an optimized modular inversion algorithm
- Zeke Medley and Panagiotis Manolios. Feedback & Synthesis in LLM-Assisted Termination Proofs
- Arend Mellendijk. A Lean Tactic for Normalizing Expressions in an Algebra over a Ring
- Valentin Mikhalchuk, Vladimir Gladshtein and Ilya Sergey. Lazy Proof Automation for Separation Logic
- Reed Mullanix and Jacques Carette. Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages
- Damien Pous. String diagrams for monoidal categories, in Rocq
- Johann Rosain and Julie Cailler. TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
- Aeacus Sheng, Wenda Li and Paul Jackson. Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)
- Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto and Naoto Onda. Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral
- Amitayush Thakur, George Tsoukalas, Greg Durrett and Swarat Chaudhuri. ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
- Dominique Unruh. Complex Bounded Operators in Isabelle/HOL
- Josef Urban. 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper)
- Eric Wang and Elif Uskuplu. Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean
- Jamie Wright, Liron Cohen, Reuben N. S. Rowe and Andrei Popescu. Certified Infinite Descent Criteria in Isabelle/HOL
- Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter and Burkhart Wolff. Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL
- Thomas Zhu, Pietro Monticone, Jeremy Avigad and Sean Welleck. LeanArchitect: Automating Blueprint Generation for Humans and AI