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,
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.