Isabelle tutorial at LIFO (Orleans)

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.

Instructors

Participants

 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

Schedule

Wednesday 24-Oct-2012

Thursday 25-Oct-2012

Course materials

System installation

Important Files

Further documentation