Isabelle tutorial at PPS

Date: Tue 10-May-2011
Time: Tue 10:00-17:00


The aim of the tutorial is to give participants a working knowledge of formal specifications and proofs in Isabelle, with the HOL logic and both tactical proof scripts and structured Isar proofs. There will be presentations by the instructors, with interactive examples and exercises for the participants on their own laptops.

The target audience are researchers and doctoral students who want to learn about interactive theorem proving in Isabelle.


Course materials

System installation

Some documentation