Hybrid event, associated with with ITP 2022 / FLoC 2022.
- Virtual Space: BigBlueButton (via TU Munich)
- Physical Location: Haifa, Israel
- Time: 11-Aug-2022
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.
Important Dates
- Paper submission deadline: 15-May-2022
- Notification of acceptance: 13-Jun-2022
- Workshop: 11-Aug-2022
Program (Haifa time / GMT+3)
- Session 09:10-10:30 (Chair: Andrei Popescu)
- 09:10 Tobias Nipkow: Welcome
- 09:20 Štěpán Holub, Štěpán Starosta and Martin Raška: Auxiliary tools for Combinatorics on Words
- 09:35 Martin Raška and Štěpán Holub: Transfer and reversal of lists (slides)
- 10:00 Olle Torstensson and Tjark Weber: Oracle Integration of Floating-Point Solvers with Isabelle (slides)
- Session 11:00-12:30 (Chair: Štěpán Holub)
- 11:00 Niels Mündler and Tobias Nipkow: A Verified Implementation of B-trees in Isabelle/HOL (slides)
- 11:30 Agnes Moesgård Eschen and Jørgen Villadsen: On Axiomatic Systems for Classical Propositional Logic (slides)
- 11:50 Asta Halkjær From: On Termination for Hybrid Tableaux (slides)
- 12:10 Frederik Krogsdal Jacobsen and Jørgen Villadsen: Lessons of Teaching Formal Methods with Isabelle (slides)
- Session 14:00-15:30 (Chair: René Thiemann)
- 14:00 Makarius Wenzel: Isabelle/VSCode and Electron/Node.js as emerging Isabelle technologies (slides)
- 14:30 Walther Neuper, Bernhard Stöger and Makarius Wenzel: Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode (slides)
- 15:00 Yecine Megdiche, Fabian Huch and Lukas Stevens: A Linter for Isabelle: Implementation and Evaluation
- Session 16:00-17:30 (Chair: Chelsea Edmonds)
- 16:00 Tobias Nipkow: Gale-Shapley Verified (slides)
- 16:30 René Thiemann: From P != NP to monotone circuits of super-polynomial size (slides)
- 17:00 Lavanya Singh: Automating Kantian Ethics in Isabelle: A Case Study (slides)
Remote Organisers
Tobias Nipkow, Larry Paulson, Makarius Wenzel