ISABELLE — PROGRAM
Days: Friday, 24 July 2026 Saturday, 25 July 2026
Friday, 24 July 2026
09:00-10:00
Keynote 1
Isabelle
Location:
C5.07
| 09:00-10:00 |
Isabelle: the last 40 years (and the next) (abstract) 60 min
1 FRS
|
10:00-10:30
Papers 1a
Isabelle
Location:
C5.07
| 10:00-10:30 |
A Tale of Two Multiset-like Types in Isabelle/HOL (abstract) 30 min
1 University of Copenhagen
|
10:30-11:00
Coffee Break
Isabelle
Location:
C5.07
11:00-12:20
Papers 1b
Isabelle
Location:
C5.07
| 11:00-11:30 |
IsaSearch: Semantic Natural-Language Search for the Archive of Formal Proofs (abstract) 30 min
1 Ludwig-Maximilians-Universität München
|
| 11:30-12:00 |
Isabelle in a Compiler-Construction Class --- Conception, Tooling, and Experiences (abstract) 30 min
1 Universite Paris-Saclay
2 University of Exeter
|
| 12:00-12:20 |
Teaching AutoCorrode in an Automated Reasoning Course (abstract) 20 min
1 Technical University of Denmark
|
12:20-14:00
Lunch
Isabelle
Location:
C5.07
14:00-15:00
Tutorial 1
Isabelle
Location:
C5.07
| 14:00-15:00 |
Isabelle/ML tool development (abstract) 60 min
1 LMU
2 UCPH
|
15:00-15:30
Papers 1c
Isabelle
Location:
C5.07
| 15:00-15:30 |
Designing a Verification Condition Generator with Eisbach and a bit of Isabelle/ML -- An experience report (abstract) 30 min
1 University of Twente
|
15:30-16:00
Coffee Break
Isabelle
Location:
C5.07
16:00-17:00
Papers 1d
Isabelle
Location:
C5.07
| 16:00-16:30 |
Mechanising Local Rely-Guarantee Reasoning over the seL4 Trace Monad (abstract) 30 min
1 The University of New South Wales
|
| 16:30-16:45 |
Two interfaces for seL4 kernel verification: Time Protection and the Kernel–Userland Gap (Extended Abstract) (abstract) 15 min
1 UNSW Sydney
|
| 16:45-17:00 |
Issues and Solutions in Autoformalization of Munkres’ Topology in Isabelle/HOL (abstract) 15 min
1 AI4REASON and University of Gothenburg
|
17:00-18:00
Panel Discussion
Isabelle
Location:
C5.07
| 17:00-18:00 |
The next 3 killer features of proof assistants in the next 10 years (abstract) 60 min
1 KCL
2 University of Exeter
3 University of Innsbruck
4 Amazon Web Services
5 AI4REASON and University of Gothenburg
|
Saturday, 25 July 2026
09:00-10:00
Keynote 2
Isabelle
Location:
C5.07
| 09:00-10:00 |
Verifying Sledgehammer backend techniques with Isabelle/HOL (abstract) 60 min
1 Loria
|
10:00-10:30
Papers 2a
Isabelle
Location:
C5.07
| 10:00-10:30 |
Earley's Recognizer: Implementation and Complexity Analysis in Isabelle/HOL (abstract) 30 min
1 Technical University of Munich
|
10:30-11:00
Coffee Break
Isabelle
Location:
C5.07
11:00-12:20
Papers 2b
Isabelle
Location:
C5.07
| 11:00-11:20 |
Formalizing the Exponential Blowup in the Transformations between CNF and DNF (abstract) 20 min
1 Ludwig-Maximilians-Universität München
|
| 11:20-11:40 |
Cracking egg: Towards Verified Equality Saturation (abstract) 20 min
1 Ludwig-Maximilians-Universität in Munich
|
| 11:40-12:00 |
Formalizing Paradoxes in Grounded Arithmetic using Isabelle/HOL (abstract) 20 min
1 EPFL
|
| 12:00-12:20 |
A Generalized Bekic Principle and its Formalization in Isabelle (abstract) 20 min
1 The Chinese University of Hong Kong
|
12:20-14:00
Lunch
Isabelle
Location:
C5.07
14:00-15:30
Tutorial 2
Isabelle
Location:
C5.07
| 14:00-15:30 |
Isabelle/Scala systems programming (abstract) 90 min
1 TUM
|
15:30-16:00
Coffee Break
Isabelle
Location:
C5.07
16:00-17:15
Papers 2c
Isabelle
Location:
C5.07
| 16:00-16:30 |
Lemmanaid: Neuro-Symbolic Lemma Conjecturing (abstract) 30 min
1 Chalmers University of Technology
2 University of California
|
| 16:30-17:00 |
Abduction Prover in Isabelle/HOL (abstract) 30 min
1 The Institute of Computer Science, the Czech Academy of Sciences
|
| 17:00-17:15 |
Safe Agentic Workflows for Isabelle (abstract) 15 min
1 King's College London
2 University of Copenhagen
3 University of Sheffield
|
17:15-18:00
Tutorial 3
Isabelle
Location:
C5.07
| 17:15-18:00 |
Exercises and Questions on Isabelle/ML and Isabelle/Scala programming (abstract) 45 min
1 UCPH
2 TUM
|