Date: Fri 23-May-2014 (8:30-12:30).
Room: Info 4.
The aim of the tutorial is to give participants a condensed overview of the Isabelle environment for interactive theorem proving: the logical framework for Natural Deduction, the Isar language for structured proofs, the HOL logic for specifications, and add-on tools that are available in the Prover IDE. There will be presentations with interactive examples and exercises for the participants.
The target audience are students and researchers with an interest in learning more about the greater LCF family of proof assistants, of which both Isabelle and Coq are members.
|Alex Auvolat||ENS Paris|
|Amir-hossein Bateni||ENS Paris|
|Anne Bouillard||ENS Paris|
|Guillaume Baudart||ENS Paris|
|Basile Clement||ENS Paris|
|Diane Gallois-Wong||ENS Paris|
|Jonathan Laurent||ENS Paris|
|Kenji Maillard||ENS Paris|
|Thomas Magnard||ENS Paris|
|Élie Michel||ENS Paris|
|Mendes Oulamara||ENS Paris|
|Raphaël Rieu-Helft||ENS Paris|
|Sigurd Schneider||Saarland University|
|Marc de Visme||ENS Paris|
|Luca Wehrstedt||ENS Paris|
During the course we are using a special Isabelle version that is a preview of Isabelle2014 (a few months before its official release).
Quick start example: after starting up Isabelle/jEdit,
the Documentation panel provides some Examples at the
bottom of the list (like
src/HOL/ex/Seq.thy). Note that jEdit
can open URLs like
but the resulting buffer will be read-only: it needs to be saved locally
Transitivite_et_Connexite.thyand its final proof document.