A Practical Isabelle/HOL Tutorial at CICM 2015

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:
  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).
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 document).