• Where: Lisbon (Portugal), associated with ITP 2026 and IJCAR 2026, as part of FLoC 2026.
• When: 24..25-Jul-2026 (UTC+1).
• Physical Location: C5.07
• Virtual Location: BigBlueButton (via TU Munich)

Call for Papers

This informal workshop will bring together users and developers of the interactive theorem prover Isabelle. The year 2026 is special due to 40th anniversary of Isabelle, so we allocate 2 full days for the event.

Regular contributors will present their research and projects, including applications of Isabelle, internal developments, add-on tools, and reports on work in progress. Invited speakers will give keynote lectures and tutorials on the Isabelle system and its culture. There will also be opportunities to discuss the past, present, and future of the Isabelle community.

Please submit a regular paper (or extended abstract) of 2–20 pages (PDF). Reviews will be informal, to check that papers are on-topic and to decide the length of the presentation slot. No formal proceedings will be published, but accepted papers and slides will be made available on the workshop website.

Important Dates

• Paper submission deadline: 09-May-2026 (AoE)
• Notification of acceptance: 01-Jun-2026 (UTC+0)
• Deadline for final versions: 15-Jun-2026 (AoE)
• Workshop: 24..25-Jul-2026

Program (Lisbon / UTC+1)

1. Day Fri 24-Jul-2026
   1. Session 09:00–10:30 (Chair: Jasmin Blanchette)
      • 09:00–10:00 Keynote by Lawrence Paulson: Isabelle: the last 40 years (and the next) (slides).
      • 10:00–10:30 Paper by Mathias Schack Rabing (speaker), Dmitriy Traytel: A Tale of Two Multiset-like Types in Isabelle/HOL.
   2. Session 11:00–12:20 (Chair: Fabian Huch)
      • 11:00–11:30 Paper by Fabian Kadlez (speaker), Balazs Toth: IsaSearch: Semantic Natural-Language Search for the Archive of Formal Proofs (slides).
      • 11:30–12:00 Paper by Achim D. Brucker, Burkhart Wolff (speaker): Isabelle in a Compiler-Construction Class — Conception, Tooling, and Experiences (slides).
      • 12:00–12:20 Paper by Örs Nagy, Jónas Mittún Peltonen, Jørgen Villadsen (speaker): Teaching AutoCorrode in an Automated Reasoning Course.
   3. Session 14:00–15:30 (Chair: Martin Desharnais-Schäfer)
      • 14:00–15:00 Tutorial by Jasmin Blanchette, Dmitriy Traytel: Isabelle/ML tool development (slides).
      • 15:00–15:30 Paper by Peter Lammich: Designing a Verification Condition Generator with Eisbach and a bit of Isabelle/ML — An experience report (slides).
   4. Session 16:00–18:00 (Chair: Jørgen Villadsen)
      • 16:00–16:30 Paper by Yousef Alhessi (speaker), Emily First, Sorin Lerner, Sólrún Halla Einarsdóttir, George Granberry, Moa Johansson, Nicholas Smallbone: Lemmanaid: Neuro-Symbolic Lemma Conjecturing.
      • 16:30–16:45 Paper by Rob Sison: Two interfaces for seL4 kernel verification: Time Protection and the Kernel–Userland Gap (Extended Abstract) (slides).
      • 16:45–17:00 Paper by Josef Urban: Issues and Solutions in Autoformalization of Munkres’ Topology in Isabelle/HOL.
      • 17:00–18:00 Panel discussion by Mohammad Abdulaziz (chair), Achim D. Brucker, Manuel Eberl, Dominic Mulligan, Josef Urban: The next 3 killer features of proof assistants in the next 10 years.
2. Day Sat 25-Jul-2026
   1. Session 09:00–10:30 (Chair: Dmitriy Traytel)
      • 09:00–10:00 Keynote by Sophie Tourret: Verifying Sledgehammer backend techniques with Isabelle/HOL.
      • 10:00–10:30 Paper by Tobias Nipkow (speaker), Alexander Haberl: Earley’s Recognizer: Implementation and Complexity Analysis in Isabelle/HOL.
   2. Session 11:00–12:20 (Chair: Sophie Tourret)
      • 11:00–11:20 Paper by Leon Raffael Schulz (remote speaker), Martin Desharnais-Schäfer, Jan Johannsen: Formalizing the Exponential Blowup in the Transformations between CNF and DNF.
      • 11:20–11:40 Paper by Alexandra Graß: Cracking egg: Towards Verified Equality Saturation.
      • 11:40–12:00 Paper by Ananthajit Srikanth (speaker), Bryan Ford: Formalizing Paradoxes in Grounded Arithmetic using Isabelle/HOL (slides).
      • 12:00–12:20 Paper by Jun Xu (remote speaker): A Generalized Bekič Principle and its Formalization in Isabelle.
   3. Session 14:00–15:30 (Chair: Makarius Wenzel)
      • 14:00–15:30 Tutorial by Fabian Huch: Isabelle/Scala systems programming (slides).
   4. Session 16:00–18:00 (Chair: Peter Lammich)
      • 16:00–16:30 Paper by Junming Zhao: Mechanising Local Rely-Guarantee Reasoning over the seL4 Trace Monad (slides).
      • 16:30–17:00 Paper by Yutaka Nagashima (speaker), Daniel Sebastian Goc: Abduction Prover in Isabelle/HOL.
      • 17:00–17:15 Paper by Maximilian Schäffeler, Lukas Stevens (speaker), Kevin Kappelmann, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel: Safe Agentic Workflows for Isabelle.
      • 17:15–18:00 Tutorial by Dmitriy Traytel, Fabian Huch: Exercises and Questions on Isabelle/ML and Isabelle/Scala programming.

Organisers and Program Chairs

• Jasmin Blanchette
• Dmitriy Traytel
• Makarius Wenzel