Call for Papers
This informal workshop is intended to bring together Isabelle users and developers. Participants are invited to 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-Apr-2018
- Notification of acceptance: 15-May-2018
- Workshop: 13-Jul-2018
Presented Papers
- Mathias Fleury, Jasmin Christian Blanchette and Peter Lammich: A Verified SAT Solver with Watched Literals Using Imperative HOL
- Andreas Lochbihler and Pascal Stoop: Lazy Algebraic Types in Isabelle/HOL
- Max W. Haslbeck and René Thiemann: Formal Verification of Bounds for the LLL Basis Reduction Algorithm
- Benedikt Stock, Abhik Pal, Maria Antonia Oprea, Yufei Liu, Malte Sophian Hassler, Simon Dubischar, Prabhat Devkota, Yiping Deng, Marco David, Bogdan Ciurezu, Jonas Bayer and Deepak Aryal: Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
- Makarius Wenzel: Further Scaling of Isabelle Technology
- Andreas Halkjær From, Anders Schlichtkrull and Jørgen Villadsen: Drawing Trees
- Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull and Jørgen Villadsen: Substitutionless First-Order Logic: A Formal Soundness Proof
- Christian Sternagel: The remote_build Tool
- Yutaka Nagashima and Yilun He: PaMpeR: A Proof Method Recommendation System for Isabelle/HOL
- Joshua Bockenek, Peter Lammich, Yakoub Nemouchi and Burkhart Wolff: Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
Organisers
Tobias Nipkow, Larry Paulson, Makarius Wenzel