Isabelle/HOL tutorial at LRI

Date: Mon 14-May-2012 (9:30-17:30) and Tue 15-May-2012 (9:30-17:30)

The aim of the tutorial is to give participants a working knowledge of formal specifications and proofs in Isabelle/HOL, using a release candidate of Isabelle2012 with the new Prover IDE. There will be presentations by the instructors, with interactive examples and exercises for the participants on their own laptops.

On the first day we give a comprehensive introduction to Isabelle/HOL in general, especially for people who have not used any other proof assistant before. On the second day, we continue at a more advanced level, especially for users of Coq. In any case, people are welcome to participate on both days.

The target audience are researchers and doctoral students who want to learn about Isabelle/HOL, structured proofs in Isabelle/Isar, and interactive theorem proving in general.

The course is organized by the ForTesSE group (Univ. Paris-Sud, LRI) and will take place in Room 435, Building 650 (PCRI) of the LRI at Platau Saclay. See the subsequent Google map for details, but note that Google still shows a field north of Rue Noetzlin where the new LRI building is now. Take Mobicabs Bus #9 from Le Guichet station (RER B) to IUT Pole d'Ingenierie (5min).

Enlarge map

Some local hotels

Instructors

Confirmed participants

MonTue Virginia AponteCNAM
MonTue Holger BlasumSYSGO, Mainz
MonTue Maria ChristofiGemalto / University of Versailles
Tue Pierre CourtieuCNAM
MonTue Frédéric DabrowskiLIFO, University of Orleans
MonTue Ali Ed-DbaliLIFO, University of Orleans
MonTue Lourdes Del Carmen González HuescaUniversité Paris 7
MonTue Mohamed HiliaUniversité Paris-Est Créteil
MonTue Bilal KansoSupélec
MonTue Bruno LangensteinDFKI, Saarbrücken
Mon Julia LawallINRIA Rocquencourt
Mon Frédéric LoulergueLIFO, University of Orleans
MonTue Yakoub NemouchiUniversité Paris 12
Mon Thomas PinsardLIFO, University of Orleans
MonTue Idir Ait SadouneSupélec
MonTue Safouan TahaSupélec
Tue Enrico TassiINRIA Saclay / Ecole Polytechnique
MonTue Nguyen Tran TrungTelecom ParisTech

Schedule

Monday 14-May-2012

Tuesday 15-May-2012

Course materials

Important Files

System installation

Some documentation