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:

1. Recursion and induction
   The initial introduction concentrates on defining small functional programs and proving properties about them by induction.
2. Logic and Automation
   This section introduces more of the logic and the available automation, including the famous Sledgehammer that harnesses external automatic theorem provers.
3. 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).

See also Programming and Proving with Isabelle/HOL.

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.