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

- Makarius Wenzel (LRI - Univ Paris-Sud)
- Abdou Feliachi (LRI - Univ Paris-Sud)

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 |

Catherine DUBOIS | ENSIIE |

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 |

**9:30-10:30**Session 1**10:30-11:00**Coffee break**11:00-12:30**Session 2**12:30-14:00**Lunch break**14:00-15:30**Session 3**15:30-16:00**Coffee break**16:00-17:30**Session 4

**9:00-10:30**Session 5**10:30-11:00**Coffee break**11:00-12:30**Session 6**12:30-14:00**Lunch break

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 command line.Linux users should note that they need to run the proper

**32 or 64 bit**version for their respective platform!-
Quick start example: open

`Seq.thy`

via Isabelle/jEdit. The screenshot shows the situation after activating the*Output*and*Sidekick*panels, and hovering with the mouse over the occurrence of`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 like

`Seq.thy`

directly, but the resulting buffer will be read-only. It needs to be saved locally before editing.

**Worksheets with exercises and solutions**- Aspects of Isabelle (Slides)
- Synopsis of Isabelle/Isar proof language elements.
- Specifications in Isabelle/HOL.
- Compact overview of Isabelle/HOL Main library.
- The extremely dense Isabelle/Isar quick reference card.
- Example material based on
*Compiling exceptions correctly*(by G. Hutton and J. Wright):- Regular paper with the main specifications and proofs in LaTeX.
- Extended paper too see even more informal proofs (optional).
- Formalization in Coq by C. Dubois.
- Formalization in Isabelle by T. Nipkow.

- The Isabelle Framework — extended abstract and overview of main literature (2008).
- The bulky Isabelle/Isar reference manual.
- Some tutorial on Isabelle/HOL.
- How to prove it: overview of common informal techniques.