Isabelle Home Page


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.

Important Dates

Submission deadline: May 11, 2014
Notification of acceptance: May 25, 2014
Workshop: July 13, 2014

Program Committee


Most of the paper reviewing was conducted with the help of CoCon, a small conference management system with confidentiality guarantees verified in Isabelle.