Isabelle tutorial at LRI in 3 Parts
Presenter:
The aim of the tutorial is to give participants a working knowledge of
formal specifications and proofs
in Isabelle, with the HOL
logic and both tactical proof scripts and structured Isar proofs.
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 interactive theorem proving in Isabelle.
Part I : Isabelle, HOL, and Specification Constructs in HOL
Date: Mon 15-Sept-2014
Time: Mon 9:00-12:00
Room: PCRI 42
Part II : Basic Proof Techniques for HOL
Date: Mon 15-Oct-2014
Time: Mon 9:00-12:00
Room: PCRI 42
Part III : Advanced Proof Techniques for HOL
Date: Mon 25-Nov-2014
Time: Mon 9:00-12:00
Room: PCRI 42
Course materials
System installation
-
The working version is Isabelle13-2. See
Older Versions.
The official version Isabelle2014
download might
not work EXACTLY for the examples. We use Isabelle/jEdit for the tutorial: it
can be started via isabelle jedit A.thy B.thy on the command
line.
- Quick start sample
files:
Seq.thy
and Editor.thy to be opened
with Isabelle/jEdit.
- Here is an example screenshot, after opening
the Output and Sidekick panels, and hovering with
the mouse over the type of
conc while holding
CONTROL/COMMAND. If it looks completely different on your system,
then there is something wrong with the installation.
Some documentation
- Extended
abstract and overview of main literature (2008).
- All other system documentation comes with the system and can be accessed
via the documentation pane in Isabelle/jedit.
- Brief overview of the Isabelle/Pure
framework.
- Synopsis of
Isabelle/HOL Main
library.
Files / Exercise Material
- Material by Burkhart:
- System Framework,
Logical Framework,
Intro HOL,
- Forward Proofs,
Basic Backward Proofs,
Advanced Backward Proofs,
- Advanced Proof Procedures,
Structured Proofs,
History of ITP Systems
- demo1,
demo2,
demo3,
demo4,
demo5,
- Material by Makarius:
