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

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


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).



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

Confirmed participants

Cedric AugerINRIA Saclay, France
Lukas BrüggerETH Zürich, Switzerland
Evelyne ContejeanINRIA Saclay and LRI, France
Paolo HermsINRIA Saclay, France
Clément HoutmannINRIA Saclay, France
Chantal KellerINRIA Saclay and École Polytechnique, France
Matthias KriegerUniv. Paris-Sud, France
Stéphane LescuyerINRIA Saclay, France
Delphine LonguetUniv. Paris-Sud, France
Pierre NeronÉcole Polytechnique, France
Jan Oliver RingertRWTH Aachen, Germany
Wendi UrribarriUniv. Paris-Sud, France
Burkhart WolffUniv. Paris-Sud, France
Jie YangUniv. Paris-Sud, France / Zhejiang University, China


Tuesday 23-Nov-2010

Wednesday 24-Nov-2010

Course material

System installation