Date: Wed 24-Oct-2012 (9:30-17:30) and Thu 25-Oct-2012 (9:00-12:30)
Room: Salle de réunion 1
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/HOL and structured proofs in Isabelle/Isar. Some basic understanding of formal logic and exposure to other proof assistants — most notably Coq — will be helpful.
All practical work is be done with the current Isabelle2012 release and the included Prover IDE Isabelle/jEdit, which supports document-oriented proof development with asynchronous interaction and parallel proof checking.
The course is adjoined to the Journées communes LTP - LAC - LAMHA at LIFO, Orléans.
|Ali ASSAF||INRIA, Ecole polytechnique|
|Wadoud BOUSDIRA||LIFO, University of Orléans|
|Jean-François CULAT||Thalès Communications & Security|
|Frédéric DABROWSKI||LIFO, University of Orleans|
|Ali ED-DBALI||LIFO, University of Orleans|
|Kento EMOTO||University of Tokyo|
|Ludovic HENRIO||CNRS, Sophia-Antipolis|
|Nikolai KOSMATOV||CEA List|
|Frédéric LOULERGUE||LIFO, University of Orleans|
|Vitor MAGRON||LIX Ecole Polytechnique|
|André MARONEZE OLIVEIRA||IRISA, INRIA Rennes|
|Guillaume PETIOT||CEA List|
|Thomas PINSARD||LIFO, University of Orleans|
|Yann SALMON||IRISA, Université Rennes 1|
|Jérémie SALVUCCI||LIP6, UMPC|
|Julien TESSON||LACL, UPEC|
See the official Isabelle2012 website.
Please ignore any mentioning of Proof General / Emacs, as we are using
Isabelle/jEdit in the tutorial. It can be started via the main
Isabelle executable or via
isabelle jedit on the
Linux users should note that they need to run the proper 32 or 64 bit version for their respective platform!
Quick start example: open
via Isabelle/jEdit. The screenshot shows the
situation after activating the Output and Sidekick
panels, and hovering with the mouse over the occurrence
Seq in the text, while holding CONTROL (on
Linux/Windows) or COMMAND (on Mac OS) to make the tooltip appear.
Note that jEdit can open URLs
Seq.thy directly, but the
resulting buffer will be read-only. It needs to be saved locally