|
Time and Location: 29 January to 1 February 2008,
Belgrade, Serbia. Part of the Workshop
on Formal Theorem Proving.
Overview:
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).
Programme:
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.
|
