Giens, France, September 2-13, 2002
Lecture Notes
The lecture notes appeared as an INRIA report.
Additional
material, such as copies of slides and introductions to the systems,
were available as separated documents.
Contents (pdf file)
Foreword (pdf file)
Introduction and Background:
Benjamin Werner and Gilles Dowek, Inria:
Proofs, Proof development, Logic, and Lambda-calculus
pdf file
Herman Geuvers, Nijmegen: Pure Type Systems (not included)
Thierry Coquand, Chalmers:
Inductive Definitions and Type Theory: an Introduction
ps file,
pdf file
Systems:
- An overview of each of the two proof assistants to be used in
the course, including some short developments of actual proofs:
Benjamin Werner, Inria: The Coq system (not included)
Tobias Nipkow, München: The Isabelle/HOL system (not included)
- A few other systems and man-machine interfaces:
Paul Callaghan, Durham: Plastic (not included)
Catarina Coquand and Thomas Hallgren, Chalmers: Alfa and Agda
ps file,
pdf file
Christophe Raffalli, Chambery:
PhoX
ps file,
pdf file
Carsten Schuermann, Yale:
Twelf
ps file,
pdf file
Laurent Théry, Inria: A quick overview of PVS and HOL (not included)
David Aspinall, Edinburgh:
Proof General: a general man-machine interface for proof assistants
ps file,
pdf file
Yves Bertot, Inria:
PCoq, a man-machine interface dedicated to Coq
ps file,
pdf file
Advanced Topics:
Per Martin-Löf, Stockholm: Informal Semantics of Type Theory (not included)
Peter Dybjer, Chalmers: Dependant Types in Programming
Susanne Graf, Verimag: Model Checking, Abstractions (not included)
Gregory Morrisett, Cornell:
Proof-Carrying Code
ps file,
pdf file
Davide Sangiorgi, Inria:
Types for Mobile Process
ps file,
pdf file
Applications:
Martin Abadi, UCSC: Security (not included)
Paul Jackson, Edinburgh: Hardware Verification (not included)
Laurent Théry, Inria: Formalised Mathematics (not included)
Slides
Martin Abadi, UCSC: Security
pdf file
Paul Callaghan, Durham: Coercions in Plastic;
ps file,
pdf file.
Thierry Coquand, Chalmers: Inductive Definitions and Type Theory
Part I,
Part II,
Part III (ps files).
Peter Dybjer, Chalmers: Dependant Types in Programming;
ps files in 2 versions:
1 slide per page -
4 slides per page
Susanne Graf, Verimag: Model Checking: algorithmic verification of
reactive systems:
slides;
2 slides on
IF (pdf files).
Laurent Théry, Inria: Introduction to
HOL and
PVS
(gzip ps files); ps files:
HOL and
PVS
Introductions to the systems
Benjamin Werner, Inria:
The Coq system
pdf file (37 pages)
Tobias Nipkow, München: The
Isabelle/HOL system.
A compact Overwiew of Structured Proofs in Isar/HOL;
ps file.
Yves Bertot, Inria: Proof development using Pcoq;
ps file,
gzip ps file
Paul Callaghan, Durham: Coercions in Plastic;
ps file