Isabelle tutorial at ENS Paris

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.

Instructors

Participants

 Alex Auvolat ENS Paris
 Amir-hossein Bateni ENS Paris
 Anne Bouillard ENS Paris
 Guillaume Baudart ENS Paris
 Basile Clement ENS Paris
 Pierre-Evariste Dagand INRIA
 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
 Xavier Rival INRIA/ENS/CNRS
 Gabriel Scherer INRIA
 Sigurd Schneider Saarland University
 Marc de Visme ENS Paris
 Luca Wehrstedt ENS Paris

Course materials

0. System installation

1. Worksheets with exercises and solutions

2. Important Files

3. Further documentation