Date: Tue 23-Nov-2010 and Wed 24-Nov-2010Presenters:
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").
|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|
Seq.thyto be opened with Isabelle/jEdit.
concwhile holding CONTROL/COMMAND. If it looks completely different on your system, then there is something wrong with the installation.