Belgrade 2008 - Tutorial

isabelle logo

Introduction to the Isabelle Proof Assistant

Clemens Ballarin


Time and Location: 29 January to 1 February 2008, Belgrade, Serbia.  Part of the Workshop on Formal Theorem Proving.

This four-day tutorial is an in-depth introduction to  the state-of-the-art proof assistant Isabelle and its use. The tutorial aims at researchers in computer science and mathematics who want to use Isabelle for a particular formalisation task, or who want to get an overview of current proof assistant technology. The following themes will be covered: lambda-calculus, introduction to natural deduction, specification tools, automated proof tools and Isabelle's language of readable proofs (Isar).

The tutorial will comprise six lectures, which are interleaved with sessions where participants work with Isabelle. Isabelle supports various logics including Higher-Order Logic (HOL) and Zermelo-Fraenkel Set Theory (ZF). The tutorial is based on HOL, but much of the presented material also applies to ZF.

  • Session I: Basics
    Brief introduction to formal verification with provers and suitable soundness architectures. This session will also cover essential technicalities needed to get started with Isabelle.
  • Session II: Lambda-Calculus
    Typed and untyped lambda-calculus.
  • Session III: Types & Natural Deduction
    Isabelle's type system, natural deduction proofs, proof scripts, higher-order unification, (classical) proof procedures and automation.
  • Session IV: Readable Proofs
    Introduction to Isabelle's language of readable proofs (Isar).
  • Session V: Inductive Definitions & Rule Induction
    Sets in Isabelle HOL, inductive definitions, proof methods for case analysis and induction.
  • Session VI: HOL as a Programming Language
    Defining types, primitive recursion, more induction, general recursion, code generation.

Target audience:
Doctoral students and researchers in computer science or mathematics who want to use Isabelle for a particular formalisation task, or who want to get an overview of the capabilities of a state-of-the-art proof assistant. Standard mathematical knowledge but no previous experience with formal methods is required.