Types Summer School '02 - Memo
This page is intended to internal use. This is a
memo for the Types Summer School '02. The point is to
present which resources are made available that best
illustrates lectures' contents. Many lecture notes should be
available at http://www-sop.inria.fr/certilab/types-sum-school02/Lnotes.
Yet, it's good to know that there is a printed version of most
slides and lecture notes in 506. I put here sample exercises
from lab sessions (in Coq and Isabelle) also additional
pointers (like Martin-Lof's slides or other references). I also
have hand-written notes in English for presentations from
Monday 2 to Tuesday 10.
Introduction to Type Theory
Benjamin Werner-Introduction to Type Theory
(lecture notes are available in 506)
Proof General
David Aspinall-Proof General
(tutorial on the internet, Proof General is available on tuba /usr/local/share/xemacs/ProofGeneral)
Coq
Benjamin Werner-Calculus of Inductive Constructions, Introduction to Coq
Yves Bertot-Pcoq
(lecture notes are available in 506, Coq is installed on tuba /usr/local/bin/coqtop)
(other references: online documentation --- tutorial, tutorial on recursive types, reference manual, standard library, coq'art; lecture notes)
Lab Sessions
lundi.html
mardi.v
0
1
2
3
Type Systems
Herman Geuvers-Type Systems (slides: 1 2 3)
Inductive Definitions
Thierry Coquand-Inductive Definitions and Type Theory (lecture notes available in 506)
(other references: Introduction to inductive definitions and
type theory ind;
Martin-Lof's monomorphic type theory and its
implementation coquand94type)
Tait Computability Method
Randy Pollack (no lecture notes, papers with similar contents: 1 2)
Dependent Types in Programming
Peter Dybjer
(lecture notes available in 506)
Isabelle and Isar
Tobias Nipkow (paper with similar contents: 1)
Lab Sessions
0
1
2
Types and Security
Martin Abadi (some addtional references: hac, trust, lecture notes should be available at http://www.cse.ucsc.edu/~abadi/Types02.pdf)
Plastic
Paul Callaghan
(lecture notes available in 506)
Informal Semantics of Type Theory
Per Martin-Lof, slides:
Formalized Mathematics, PVS, HOL
Laurent Thery
(lecture notes available in 506)
Agda, Alfa
Catarina Coquand (Introduction to structured type theory, the Agda interactive proof editor and its graphical interface Alfa)
TAL
Gregory Morrisett (no lecture notes)
Hardware Verification
Paul Jackson (lecture notes available in 506)