ITP — PROGRAM
Days: Sunday, 26 July 2026 Monday, 27 July 2026 Tuesday, 28 July 2026 Wednesday, 29 July 2026
Sunday, 26 July 2026
10:00-11:00
Coffee Break
ITP
Location:
B1.04
11:00-12:00
ITP Papers: Formalisation of Mathematics
ITP
Location:
B1.04
| 11:00-11:30 |
Complex Bounded Operators in Isabelle/HOL (abstract) 30 min
1 RWTH Aachen, University of Tartu
|
| 11:30-12:00 |
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral (abstract) 30 min
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
Location:
B1.04
| 14:00-14:30 |
Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations (abstract) 30 min
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
1 INRIA
2 PQShield
|
| 15:00-15:30 |
Verification of the Garsia–Wachs Algorithm (abstract) 30 min
1 Hosei University
|
15:30-16:30
Coffee Break
ITP
Location:
B1.04
16:30-17:50
ITP Papers: Program Logics
ITP
Location:
B1.04
| 16:30-17:00 |
Title: Fractional Separation Logic in Isabelle/LLVM (abstract) 30 min
1 University of Twente
|
| 17:00-17:30 |
Lazy Proof Automation for Separation Logic (abstract) 30 min
1 National University of Singapore
|
| 17:30-18:00 |
Formalizing a Hoare Calculus for Choreographic Programming (abstract) 30 min
1 IT University of Copenhagen
2 Independent Researcher
|
Monday, 27 July 2026
09:00-10:00
ITP Invited Talk: Dominic Mulligan, Amazon Web Services
ITP
Location:
B1.04
10:00-11:00
Coffee Break
ITP
Location:
B1.04
11:00-12:00
ITP Papers: Verification and Model Checking
ITP
Location:
B1.04
| 11:00-11:30 |
Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL (abstract) 30 min
1 University of York
2 Université Paris-Saclay
|
| 11:30-12:00 |
Securing the Foundations of an Intermediate Language for Probabilistic Program Verification (abstract) 30 min
1 Technical University of Denmark
2 University of Oldenburg and Technical University of Denmark
|
12:00-14:00
Lunch
ITP
Location:
B1.04
14:00-15:30
ITP Papers: AI and ITP
ITP
Location:
B1.04
| 14:00-14:30 |
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving (abstract) 30 min
1 University of Texas at Austin
2 New York University
|
| 14:30-15:00 |
Feedback & Synthesis in LLM-Assisted Termination Proofs (abstract) 30 min
1 Northeastern University
|
| 15:00-15:30 |
LeanArchitect: Automating Blueprint Generation for Humans and AI (abstract) 30 min
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
Location:
B1.04
| 16:30-17:00 |
Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean (abstract) 30 min
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
1 Massachusetts Institute of Technology
|
| 17:20-17:40 |
Formal Primal-Dual Algorithm Analysis (Short Paper) (abstract) 20 min
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
1 AI4REASON and University of Gothenburg
|
18:00-19:00
Business meeting: AI and ITP conference Series
ITP
Location:
B1.04
19:00-20:00
AI for Math Happy Hour (“Differentiated” Networking)
ITP
Location:
B1.04
Tuesday, 28 July 2026
10:00-11:00
Coffee Break
ITP
Location:
B1.04
11:00-12:00
ITP Papers: Proof Theory and Types
ITP
Location:
B1.04
| 11:00-11:30 |
Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees (abstract) 30 min
1 Portland State University
|
| 11:30-12:00 |
Bidirectional Interpolation for the Lambda-Calculus – Revisiting and Formalising Craig-Čubrić Interpolation (abstract) 30 min
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
Location:
B1.04
| 14:00-14:30 |
Enhancing Interactive Theorem Prover Error Messages with Hints (abstract) 30 min
1 Delft University of Technology
|
| 14:30-15:00 |
Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language (abstract) 30 min
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
1 McMaster University
|
15:30-16:30
Coffee Break
ITP
Location:
B1.04
16:30-18:00
ITP Papers: Automation and Tactics
ITP
Location:
B1.04
| 16:30-16:50 |
A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper) (abstract) 20 min
1 University of Bonn
|
| 16:50-17:10 |
Lean on Vampire Proofs (Short Paper) (abstract) 20 min
1 TU Wien
2 University of Southampton
|
| 17:10-17:40 |
TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq (abstract) 30 min
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
1 University of Edinburgh
|
Wednesday, 29 July 2026
09:00-10:00
ITP Invited Talk: Dominique Unruh, RWTH Aachen and University of Tartu
ITP
Location:
B1.04
10:00-11:00
Coffee Break
ITP
Location:
B1.04
11:00-12:00
ITP Paper: Automata and Coinduction
ITP
Location:
B1.04
| 11:00-11:30 |
Completing Almost Fair Simulations (abstract) 30 min
1 CISPA Helmholtz Center for Information Security
|
| 11:30-12:00 |
Certified Infinite Descent Criteria in Isabelle/HOL (abstract) 30 min
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
Location:
B1.04
| 14:00-14:30 |
Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean (abstract) 30 min
1 University of Connecticut
2 Universität Regensburg
|
| 14:30-15:00 |
From Weierstraß to Dedekind: Formalising Foundations of Modular Forms (abstract) 30 min
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
1 Carnegie Mellon University
|
15:30-16:30
Coffee Break
ITP
Location:
B1.04
16:30-18:00
ITP Papers
ITP
Location:
B1.04
| 16:30-17:00 |
Formally Verified Liveness with Multiparty Session Types in Rocq (abstract) 30 min
1 University of Edinburgh
2 University of Oxford
|
| 17:00-17:30 |
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar (abstract) 30 min
1 University of Iowa
2 Stanford University
|
| 17:30-18:00 |
String diagrams for monoidal categories, in Rocq (abstract) 30 min
1 ENS de Lyon
|