- Virtual Space: private channel
- Physical Location: Tbilisi (Georgia), Room 115
- Time:
13-Sep-202414-Sep-2024 - Paper submission deadline: 16-Jun-2024 (AoE)
- Notification of acceptance: 02-Jul-2024
- Deadline for final versions: 11-Aug-2024 (AoE)
- Workshop: 14-Sep-2024
- Session 09:20-10:30 (Chair: Tobias Nipkow)
- 09:20 Welcome by Tobias Nipkow
- 09:30 Jamie Wright and Andrei Popescu: A formalized programming language with speculative execution (slides)
- 10:00 Artur Graczyk, Marialena Hadjikosti and Andrei Popescu: A programming language for controlling robots (work in progress)
- Session 11:00-12:30 (Chair: Frédéric Blanqui), joint session with EuroProofNet Workshop
- 11:00 Makarius Wenzel: Isabelle proof terms revisited (slides)
- 11:30 Fabian Huch: Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds (slides)
- 12:00 Achim D. Brucker, Idir Ait-Sadoune, Nicolas Méric and Burkhart Wolff: Isabelle/DOF: Extended Abstract and Tool Demonstration (slides)
- Session 14:00-15:30 (Chair: Fabian Huch), joint session with EuroProofNet Workshop
- 14:00 Invited talk by Freek Wiedijk: From 100 to 1000+ theorems (slides)
- 15:00 Ghilain Bergeron, Stéphane Glondu and Sophie Tourret: HOL Light to Isabelle/HOL Translation, Rebooted
- Session 16:00-18:00 (Chair: Manuel Eberl)
- 16:00 René Thiemann: Verified Preprocessing of Linear Integer Arithmetic Constraints (slides)
- 16:30 Rafael Castro Gonçalves Silva and Dmitriy Traytel: Time-Aware Stream Processing in Isabelle/HOL (slides)
- 17:00 Frederik Krogsdal Jacobsen and Jørgen Villadsen: A Formalization of Sequent Calculus for Classical Implicational Logic (slides)
- 17:30 Jonathan Julian Huerta Y Munive: Project Proposal: Reinforcement learning on the Isabelle proof assistant (slides)
Hybrid event, associated with ITP 2024.
Call for Papers
This informal workshop will bring together users and developers of the interactive theorem prover Isabelle. Participants will present their research and projects, including applications of Isabelle, internal developments, add-on tools, and reports on work in progress.
Please submit a paper (or extended abstract) of up to 20 pages. These will be reviewed informally and accepted papers will form part of the programme. Time permitting, the workshop will include demonstrations or briefings by the development team. There will also be opportunities to discuss issues of interest to the Isabelle community.
Papers should be submitted (in PDF) using EasyChair. No formal proceedings will be published, but accepted papers will be available on the workshop website.