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: Nitro Isolation Engine: Formally Verifying a Production Hypervisor
Dominique Unruh, RWTH Aachen and University of Tartu: Developing a quantum crypto theorem prover from scratch
Proceedings
The proceedings of the conference are available as volume 382 of LIPIcs.
Program Schedule
For the full FLoC program, including ITP, please visit the FLOC 2026 website.
Sunday, 26th July 2026
| 09:00-10:00 | FLOC Keynote: Leonardo de Moura |
| 10:00-11:00 | Coffee Break |
| Session 1: Formalisation of Mathematics. Chair: Manuel Eberl | |
| 11:00-11:30 | Dominique Unruh, José Manuel Rodríguez Caballero: 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. Chair: Yannick Forster | |
| 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. Chair: Christine Rizkallah | |
| 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 - Nitro Isolation Engine: Formally Verifying a Production Hypervisor |
| 10:00-11:00 | Coffee Break |
| Session 4: Verification. Chair: Alessandro Bruni | |
| 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 | Omer Keskin, Nobuko Yoshida, Rob van Glabbeek: Formally Verified Liveness with Multiparty Session Types in Rocq |
| 12:00-14:00 | Lunch |
| Session 5: AI and ITP. Chair: Mohammad Abdulaziz | |
| 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. Chair: Manuel Eberl | |
| 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), organised and sponsored by Renaissance Philantropy. The venue is O Lago, a pleasant 15/20 minute walk from the main venue. |
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. Chair: Ekaterina Komendantskaya | |
| 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. Chair: Matthew Daggitt | |
| 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. Chair: Jasmin Blanchette | |
| 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 - Developing a quantum crypto theorem prover from scratch |
| 10:00-11:00 | Coffee Break |
| Session 10: Automata and Coinduction. Chair: Christine Rizkallah | |
| 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. Chair: Tobias Nipkow | |
| 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. Chair: Dmitriy Traytel | |
| 16:30-17:00 | Oliver Emil Bøving, Christoph Matheja: Securing the Foundations of an Intermediate Language for Probabilistic Program Verification |
| 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 and José Manuel Rodríguez Caballero. 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