Giens, France,
August 30 - September 10, 1999
Lecture Notes
The lecture notes appear as an INRIA report.
Most of them are available electronically.
Contents
Foreword
Introduction and background:
Henk Barendregt:
The quest for correctness
Bengt Nordström:
Representing proofs and statements
Herman Geuvers:
Pure
Type Systems
Thierry Coquand:
Inductive
definitions and Type Theory
Systems:
Benjamin Werner:
The
Coq system
Zhaohui Luo:
The
Lego system
Catarina Coquand and Thomas Hallgren:
Agda,
the current version of the Alf family
Tobias Nipkow:
The Isabelle system
Avanced topics:
Per Martin-Löf: Nonstandard Type Theory
Michel Parigot: Program extraction in 2nd order classical logic
Laurent Théry:
A
quick overview of PVS and HOL
Jean-Louis Krivine:
Lambda-calculus and ZF
Stefano Berardi:
Types
and program optimization
Yves Lafont:
Linear logic and computer science
Applications:
John Harrison:
Formal verification in industry
Henrik Persson:
Certified computer algebra
Jaco van de Pol:
Proofs of correctness of protocols
Tobias Nipkow:
Formalizing and analyzing Java in Isabelle/HOL
Aarne Ranta:
Linguistic applications of type theory