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. The tutorial has three sections:
The tutorial (given by Tobias Nipkow)
will be based on Part I of the book Concrete Semantics that is
freely availble online (and is also available as this separate
- 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).