Isabelle Workshop 2016

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, etc. Well-argued position papers (e.g. describing proposed extensions) are also welcome, 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.

Timetable

Thursday 25 August 2016
14:00-15:30
14:00-14:30 Makarius Wenzel: The Isar Proof Language in 2016
14:30-15:00 Makarius Wenzel: System demonstration: Isabelle/PIDE as IDE for ML
15:00-15:30 Gergely Buday: Towards an Isar Tutorial
BREAK, 15:30-16:00
16:00-17:30
16:00-16:30 Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
16:30-17:00 Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen: Verification of an LCF-Style First-Order Prover with Equality
17:00-17:30 Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From: Code Generation for a Simple First-Order Prover
Friday 26 August 2016
9:00-10:30
9:00-9:30 Fadoua Ghourabi, Kazuko Takahashi: A Proof of the Compositions of Time Interval Relations
9:30-10:00 Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada: A Formalization of Berlekamp's Factorization Algorithm
10:00-10:30 Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel: Friends with Benefits: Implementing Foundational Corecursion in Isabelle/HOL
BREAK, 10:30-11:00
11:00-12:30
11:00-11:30 Yutaka Nagashima: Keep Failed Proof Attempts in Memory
11:30-12:00 Simon Wimmer: Smashing Isabelle: Flex-Flex Pairs in 2016
12:00-12:30 Dominik Vinan, Lars Hupel: Clone Detection in Isabelle Theories (ConQAT+Isabelle bundle (preview))

Important Dates

Organisers

Tobias Nipkow, Larry Paulson, Makarius Wenzel