- Where: In Virtual Space, associated with IJCAR 2020 and Paris Nord Summer of LoVe. (The originally planned location in Paris-Aubervilliers, France had to be cancelled.)
- When: 30-Jun-2020 (virtual event in timezone of Paris: GMT+2)
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: 16-Apr-2020
- Notification of acceptance: 15-May-2020
- Workshop: 30-Jun-2020
Program (Paris time / GMT+2)
- Session 9:30–11:00 (Chair: Tobias Nipkow, video)
- Chelsea Edmonds: Lucas’s Theorem: Formalising Generating Function Proofs (slides)
- Lawrence Paulson: Ackermann’s Function in Iterative Form: A Subtle Termination Proof with Isabelle/HOL (slides, video)
- Asta Halkjær From and Jørgen Villadsen: A Concise Sequent Calculus for Teaching First-Order Logic (slides, video)
- Session 11:30-13:00 (Chair: Makarius Wenzel)
- Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki and Lawrence Paulson: SErAPIS : A Concept-Oriented Search Engine for the Isabelle Libraries Based on Natural Language (slides)
- Fabian Huch and Alexander Krauss: FindFacts: A Scalable Theorem Search (slides)
- Clemens Ballarin: An Antiquotation for Locale Graphs
- Session 14:00–15:30 (Chair: Larry Paulson)
- Makarius Wenzel: Isabelle NEWS and trends in 2020 (slides, video)
- Andreas Lochbihler and Ognjen Marić: Authenticated Data Structures as Functors in Isabelle/HOL (slides, video)
- Martin Desharnais and Stefan Brunthaler: A Generic Framework for Verified Compilers Using Isabelle/HOL’s Locales (slides, video)
- Session 16:00–17:30 (Chair: Andreas Lochbihler)
- Yutaka Nagashima: Smart Induction for Isabelle/HOL (slides)
- Walther Neuper: Lucas-Interpretation on Isabelle’s Functions (slides)
- Frédéric Tuong and Burkhart Wolff: Isabelle/C: A Generic Front-End of C11 Supported in Isabelle/PIDE (slides, video)