Isabelle tutorial at PPS

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

Presenters:

Makarius Wenzel (Univ. Paris-Sud, LRI)
Burkhart Wolff (Univ. Paris-Sud, LRI)

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.

Schedule

10:00-12:00 Session 1
12:00-13:30 Lunch break
13:30-15:00 Session 2
15:00-15:30 Coffee break
15:30-17:00 Session 3

Course materials

System installation

See the download of official Isabelle2011. The description mostly mentions Proof General / Emacs, but we recommend Isabelle/jEdit for the tutorial: it can be started via isabelle jedit A.thy B.thy on the command line.
Quick start sample files: Seq.thy and Editor.thy to be opened with Isabelle/jEdit.
Here is an example screenshot, after opening the Output and Sidekick panels, and hovering with the mouse over the type of conc while holding CONTROL/COMMAND. If it looks completely different on your system, then there is something wrong with the installation.

Some documentation

Extended abstract and overview of main literature (2008).
The indispensible Isabelle/Isar quick reference (appendix A of the bulky Isabelle/Isar reference manual).
Brief overview of the Isabelle/Pure framework.
Synopsis of Isabelle/HOL Main library.

Files

Material by Burkhart:

U1, U2, U3, U4
demo1, demo2, demo3, demo4, demo5

Material by Makarius: