Isabelle/Isar tutorial at Univ. Paris-Sud, LRI

Date: Tue 23-Nov-2010 and Wed 24-Nov-2010

Presenters:

Christian Urban (TU Munich and Cambridge Univ.)
Makarius Wenzel (Univ. Paris-Sud, LRI)

The aim of the tutorial is to give participants a working knowledge of formal specifications and proofs in Isabelle, using the HOL logic and the Isar proof language. 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 Isabelle/Isar, or interactive theorem proving in general.

The course is organized by the ForTesSE group (Univ. Paris-Sud, LRI) and will take place at Platau Saclay in the buildings of INRIA (mainly Room N107).

Location

Plan of the Parc Club campus. The course will be in Building N (room N107) for most of the time, and Building G (room G008) on the second afternoon.
How to get to INRIA Saclay (in French).
Short version: take the local train RER B to Le Guichet, then the bus 269-02 to Parc Club.
Note that the picture with the GPS coordinates shows Building G.
Some local hotels
- in Orsay in walking distance of Parc Club (15-20min),
- in Paris with good connection via public transport (45min).

Wi-Fi

INRIA provides free Wi-Fi access for guests ("INVITES").

Confirmed participants

Cedric Auger	INRIA Saclay, France
Lukas Brügger	ETH Zürich, Switzerland
Evelyne Contejean	INRIA Saclay and LRI, France
Paolo Herms	INRIA Saclay, France
Clément Houtmann	INRIA Saclay, France
Chantal Keller	INRIA Saclay and École Polytechnique, France
Matthias Krieger	Univ. Paris-Sud, France
Stéphane Lescuyer	INRIA Saclay, France
Delphine Longuet	Univ. Paris-Sud, France
Pierre Neron	École Polytechnique, France
Jan Oliver Ringert	RWTH Aachen, Germany
Wendi Urribarri	Univ. Paris-Sud, France
Burkhart Wolff	Univ. Paris-Sud, France
Jie Yang	Univ. Paris-Sud, France / Zhejiang University, China

Schedule

Tuesday 23-Nov-2010

10:00-12:00 Session 1 (N107)
12:00-14:00 Lunch break (Note: CESFO restaurant on strike!)
14:00-15:30 Session 2 (N107)
15:30-16:00 Coffee break (next to N107)
16:00-17:30 Session 3 (N107)

Wednesday 24-Nov-2010

10:00-11:45 Session 4 (N107)
11:45-13:30 Lunch break (CESFO restaurant)
13:30-14:30 Session 5 (N107)
14:30-15:00 Coffee break (next to N107)
15:00 change to building G
15:15-17:00 Session 6 (G008)

Course material

System installation

Isabelle download specifically for the tutorial.
Quick start sample files: Editor.thy and Seq.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.

Documentation

The indispensible Isabelle/Isar quick reference (appendix A of the bulky Isabelle/Isar reference manual).
The Isabelle/Pure framework

Files

Tutorial1.thy (Christian)
Tutorial2.thy (Christian)
Tutorial_Solutions.thy (Christian)
Natural_Deduction_Solution.thy (Makarius)
Calculation_Solution.thy (Makarius)
Induction_Solution.thy (Makarius)
Elimination_Solution.thy (Makarius)
Matcher.thy (Christian)