Time and Location: 29 January to 1 February 2008,
Belgrade, Serbia. Part of the Workshop
on Formal Theorem Proving.
Overview:
This fourday tutorial is an indepth introduction to the
stateoftheart 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: lambdacalculus,
introduction to natural deduction, specification tools, automated proof
tools and Isabelle's language of readable proofs (Isar).
Programme:
The tutorial will comprise six lectures, which are interleaved with
sessions where participants work with Isabelle. Isabelle supports
various logics including HigherOrder Logic (HOL) and ZermeloFraenkel
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: LambdaCalculus
Typed and untyped lambdacalculus.
 Session III: Types & Natural Deduction
Isabelle's type system, natural deduction proofs, proof scripts,
higherorder 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 stateoftheart proof
assistant. Standard mathematical knowledge but no previous experience
with formal methods is required.
