en | de

Experiments in Verification – Introduction to Isabelle/HOL

master program

VO1  SS 2011  703523


The course provides an introduction to the proof assistant Isabelle/HOL.


The lecture is blocked. Instead of a weekly 1-hour lecture, there will be 4 sessions of 3 hours each. Related courses to some of the discussed topics are given in parentheses.

session date topics slides sources
1 11.03. formal verification, Isabelle/HOL basics, functional programming in HOL (functional programming) pdf (4x1) archive
2 25.03 simplification (term rewriting), function definitions, induction, calculational reasoning pdf (4x1) archive
3 01.04. natural deduction, propositional logic, predicate logic (logic) pdf (4x1) archive
4 15.04. (inductively defined) sets, relations, advanced topics pdf (4x1) archive


The course incorporates material from the following source: