This tutorial and workshop is centered around the interactive theorem prover Isabelle. Target audience are both novices interested in acquainting themselves with Isabelle, for example logicians, and the Isabelle user and developer community. Therefore there will be a combination of hands-on tutorial introduction to Isabelle with contributed talks from the Isabelle community. Due to the unexpectedly high number of workshop submissions there will be parallel tracks in separate rooms!
Tutorial: A Practical Introduction to Isabelle/HOL for Beginners (by Tobias Nipkow)
This is a hands-on tutorial introduction to the proof assistant Isabelle/HOL. Slide presentations alternate with practical exercises: partipants should bring their own laptop with Isabelle installed. There will be seasoned Isabelle tutors to help you using the system. The tutorial takes 3.5h and has three sections:
- Recursion and induction
The initial introduction concentrates on defining small functional programs and proving properties about them by induction.
- Logic and Automation
This section introduces more of the logic and the available automation, including the famous Sledgehammer that harnesses external automatic theorem provers.
- Structured proofs
This section introduces Isabelle's structured proof language Isar, which combines readability (via block-structured natural-deduction proofs) with conciseness (via the rich proof automation infrastructure).
NOTE: One week before the tutorial there will be a special download of a preview of Isabelle2014, specifically for this event. Watch this space.
Workshop: Call for Papers
Contributed papers of up to 20 pages should be submitted here: https://www.easychair.org/conferences/?conf=isabelle2014. Papers will be informally reviewed by the program committee, and distributed on the FLoC USB stick and workshop web page. There are no formal proceedings.
|Submission deadline:||May 11, 2014|
|Notification of acceptance:||May 25, 2014|
|Workshop:||July 13, 2014|
- Tobias Nipkow (TU München) - chair
- Larry Paulson (University of Cambridge) - chair
- Makarius Wenzel (sketis.net) - chair
Most of the paper reviewing was conducted with the help of CoCon, a small conference management system with confidentiality guarantees verified in Isabelle.