ITP — PROGRAM

Days: Sunday, 26 July 2026 Monday, 27 July 2026 Tuesday, 28 July 2026 Wednesday, 29 July 2026

Sunday, 26 July 2026
08:45-10:00 Keynote: The Lean Theorem Prover: Design, Evolution, and Impact ITP
Location: Grande Auditório
08:45-10:00
The Lean Theorem Prover: Design, Evolution, and Impact (abstract) 75 min
Leonardo de Moura
10:00-11:00 Coffee Break ITP
Location: B1.04
11:00-12:00 ITP Papers: Formalisation of Mathematics ITP
Session Chair:
Manuel Eberl
Location: B1.04
11:00-11:30
Complex Bounded Operators in Isabelle/HOL (abstract) 30 min
Dominique Unruh1, José Manuel Rodríguez Caballero2
1 RWTH Aachen, University of Tartu
2 Mathématiques et statistique – Faculté des sciences et de génie – Université Laval
11:30-12:00
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral (abstract) 30 min
Sho Sonoda1,5, Kazumi Kasaura2, Yuma Mizuno3, Kei Tsukamoto4, Naoto Onda2
1 RIKEN AIP
2 OMRON SINIC X Corporation
3 University College Cork
4 The University of Tokyo
5 CyberAgent Inc
12:00-14:00 Lunch ITP
Location: B1.04
14:00-15:30 ITP Papers: Formalisation of Algorithms ITP
Session Chair:
Yannick Forster
Location: B1.04
14:00-14:30
Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations (abstract) 30 min
Ricardo Almeida1, Blair Archibald1, Basile Pesin2, Michele Sevegnani1
1 School of Computing Science, University of Glasgow, Glasgow, Scotland
2 Fédération ENAC ISAE-SUPAERO ONERA, Université de Toulouse, France
14:30-15:00
Functional correctness of an optimized modular inversion algorithm (abstract) 30 min
Assia Mahboubi1, Guillaume Melquiond1, Pierre-Yves Strub2, Tomás Vallejos Parada1
1 INRIA
2 PQShield
15:00-15:30
Verification of the Garsia–Wachs Algorithm (abstract) 30 min
Makoto Kanazawa1
1 Hosei University
15:30-16:30 Coffee Break ITP
Location: B1.04
16:30-17:50 ITP Papers: Program Logics ITP
Session Chair:
Christine Rizkallah
Location: B1.04
16:30-17:00
Title: Fractional Separation Logic in Isabelle/LLVM (abstract) 30 min
Peter LAMMICH1
1 University of Twente
17:00-17:30
Lazy Proof Automation for Separation Logic (abstract) 30 min
Valentin Mikhalchuk1, Vladimir Gladshtein1, Ilya Sergey1
1 National University of Singapore
17:30-18:00
Formalizing a Hoare Calculus for Choreographic Programming (abstract) 30 min
Luís Cruz-Filipe1, Thomas Wulff Heissel2
1 IT University of Copenhagen
2 Independent Researcher
18:00-20:00 Reception ITP
Location: Pátio da Galé
Monday, 27 July 2026
09:00-10:00 ITP Invited Talk: Dominic Mulligan, Amazon Web Services ITP
Session Chair:
Ekaterina Komendantskaya
Location: B1.04
09:00-10:00
Nitro Isolation Engine: Formally Verifying a Production Hypervisor (abstract) 60 min
Dominic Mulligan1
1 AWS
10:00-11:00 Coffee Break ITP
Location: B1.04
11:00-12:00 ITP Papers: Verification and Model Checking ITP
Session Chair:
Alessandro Bruni
Location: B1.04
11:00-11:30
Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL (abstract) 30 min
Fang Yan1, Benoît Ballenghien2, Simon Foster1, Ana Cavalcanti1, James Baxter1, Burkhart Wolff2
1 University of York
2 Université Paris-Saclay
11:30-12:00
Formally Verified Liveness with Multiparty Session Types in Rocq (abstract) 30 min
Omer Keskin1, Nobuko Yoshida2, Rob van Glabbeek1
1 University of Edinburgh
2 University of Oxford
12:00-14:00 Lunch ITP
Location: B1.04
14:00-15:30 ITP Papers: AI and ITP ITP
Session Chair:
Mohammad Abdulaziz
Location: B1.04
14:00-14:30
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving (abstract) 30 min
Amitayush Thakur1, George Tsoukalas1, Greg Durrett2, Swarat Chaudhuri1
1 University of Texas at Austin
2 New York University
14:30-15:00
Feedback & Synthesis in LLM-Assisted Termination Proofs (abstract) 30 min
Zeke Medley1, Panagiotis Manolios1
1 Northeastern University
15:00-15:30
LeanArchitect: Automating Blueprint Generation for Humans and AI (abstract) 30 min
Thomas Zhu1, Pietro Monticone2, Jeremy Avigad1, Sean Welleck1
1 Carnegie Mellon University
2 University of Trento
15:30-16:30 Coffee Break ITP
Location: B1.04
16:30-18:00 ITP Papers: Formalisation of Mathematics & AI ITP
Session Chair:
Manuel Eberl
Location: B1.04
16:30-17:00
Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean (abstract) 30 min
Eric Jonathan Wang1, Elif Uskuplu2
1 Carnegie Mellon University
2 Indiana University Bloomington
17:00-17:20
Three Roads to de Finetti's Theorem in Lean: Short Paper (abstract) 20 min
Cameron Freer1
1 Massachusetts Institute of Technology
17:20-17:40
Formal Primal-Dual Algorithm Analysis (Short Paper) (abstract) 20 min
Thomas Ammer1, Mohammad Abdulaziz1, Christoph Madlener
1 King's College London
17:40-18:00
130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper) (abstract) 20 min
JOSEF URBAN1
1 AI4REASON and University of Gothenburg
18:00-19:00 Business meeting: AI and ITP conference Series ITP
Location: B1.04
18:00-19:00
Future of ITP Conference Series & Gen AI (discussion panel) (abstract) 60 min
Ekaterina Komendantskaya1, Tobias Nipkow2
1 Southampton
2 Munich
19:30-20:30 AI for Math Happy Hour (“Differentiated” Networking) ITP
Location: Lago Lisboa
19:30-20:30
Social Event Sponsored by Renaissance Philantropy (abstract) 60 min
Renaissance Philantropy1
1 renaissancephilanthropy
Tuesday, 28 July 2026
08:45-10:00 Keynote: Trustworthy Neuro-Symbolic Programming with Informal Specifications ITP
Location: Grande Auditório
08:45-10:00
Trustworthy Neuro-Symbolic Programming with Informal Specifications (abstract) 75 min
Işıl Dillig
10:00-11:00 Coffee Break ITP
Location: B1.04
11:00-12:00 ITP Papers: Proof Theory and Types ITP
Session Chair:
Ekaterina Komendantskaya
Location: B1.04
11:00-11:30
Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees (abstract) 30 min
Yiming Lin1, Ian Kariniemi1, Yao Li1
1 Portland State University
11:30-12:00
Bidirectional Interpolation for the Lambda-Calculus – Revisiting and Formalising Craig-Čubrić Interpolation (abstract) 30 min
Meven Lennon-Bertrand1, Alexis Saurin2
1 Université Paris Cité, INRIA, CNRS, IRIF
2 Université Paris Cité, CNRS, INRIA, IRIF
12:00-14:00 Lunch ITP
Location: B1.04
14:00-15:30 ITP Papers: User Interfaces and Compilers ITP
Session Chair:
Matthew Daggitt
Location: B1.04
14:00-14:30
Enhancing Interactive Theorem Prover Error Messages with Hints (abstract) 30 min
Maria Khakimova1, Sára Juhošová1, Jaro Reinders1, Jesper Cockx1
1 Delft University of Technology
14:30-15:00
Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language (abstract) 30 min
Vladimir Gladshtein1, K. Rustan M. Leino2
1 National University of Singapore
2 Amazon Web Services
15:00-15:30
Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages (abstract) 30 min
Reed Mullanix1, Jacques Carette1
1 McMaster University
15:30-16:30 Coffee Break ITP
Location: B1.04
16:30-18:00 ITP Papers: Automation and Tactics ITP
Session Chair:
Jasmin Blanchette
Location: B1.04
16:30-16:50
A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper) (abstract) 20 min
Arend Mellendijk1
1 University of Bonn
16:50-17:10
Lean on Vampire Proofs (Short Paper) (abstract) 20 min
Jonas Bodingbauer1, Marton Hajdu1, Laura Kovacs1, Axel Polaczek1, Michael Rawson2
1 TU Wien
2 University of Southampton
17:10-17:40
TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq (abstract) 30 min
Johann Rosain1, Julie Cailler2
1 ENS de Lyon
2 University of Lorraine, CNRS, Inria, LORIA, Nancy, France
17:40-18:00
Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper) (abstract) 20 min
Aeacus Sheng1, Wenda Li1, Paul Jackson1
1 University of Edinburgh
19:00-23:00 Banquet ITP
Location: Pavilhão Carlos Lopes
Wednesday, 29 July 2026
09:00-10:00 ITP Invited Talk: Dominique Unruh, RWTH Aachen and University of Tartu ITP
Session Chair:
Tobias Nipkow
Location: B1.04
09:00-10:00
Developing a quantum crypto theorem prover from scratch (abstract) 60 min
Dominic Unruh1
1 Aachen
10:00-11:00 Coffee Break ITP
Location: B1.04
11:00-12:00 ITP Paper: Automata and Coinduction ITP
Session Chair:
Christine Rizkallah
Location: B1.04
11:00-11:30
Completing Almost Fair Simulations (abstract) 30 min
Arthur Correnson1, Iona Kuhn1, Bernd Finkbeiner1
1 CISPA Helmholtz Center for Information Security
11:30-12:00
Certified Infinite Descent Criteria in Isabelle/HOL (abstract) 30 min
Jamie Wright1, Liron Cohen2, Reuben N. S. Rowe3, Andrei Popescu1
1 University of Sheffield
2 Ben-Gurion University of the Negev
3 Royal Holloway University of London
12:00-14:00 Lunch ITP
Location: B1.04
14:00-15:30 ITP Papers: Formalisation of Mathematics-3 ITP
Session Chair:
Tobias Nipkow
Location: B1.04
14:00-14:30
Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean (abstract) 30 min
Garett Cunningham1, Daniel Zach2, Stefan Friedl2
1 University of Connecticut
2 Universität Regensburg
14:30-15:00
From Weierstraß to Dedekind: Formalising Foundations of Modular Forms (abstract) 30 min
Manuel Eberl1, Wenda Li2, Lawrence C. Paulson3
1 University of Innsbruck
2 University of Edinburgh
3 University of Cambridge
15:00-15:30
An End-to-End Verification of Keller's Conjecture (abstract) 30 min
James Gallicchio1, Cayden Codel1, Jeremy Avigad1, Marijn J. H. Heule1
1 Carnegie Mellon University
15:30-16:30 Coffee Break ITP
Location: B1.04
16:30-18:00 ITP Papers ITP
Session Chair:
Dmitriy Traytel
Location: B1.04
16:30-17:00
Securing the Foundations of an Intermediate Language for Probabilistic Program Verification (abstract) 30 min
Oliver Emil Bøving1, Christoph Matheja2
1 Technical University of Denmark
2 University of Oldenburg and Technical University of Denmark
17:00-17:30
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar (abstract) 30 min
Sage Binder1, Hanna Lachnitt2, Katherine Kosaian1
1 University of Iowa
2 Stanford University
17:30-18:00
String diagrams for monoidal categories, in Rocq (abstract) 30 min
Damien Pous1
1 ENS de Lyon
Designed and Developed by EventKey | Copyright 2026 EventKey Last updated: · Local time:
🔍
↑