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)


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)


Paul Callaghan (lecture notes available in 506)

Informal Semantics of Type Theory

Per Martin-Lof, slides:
1 2 3 4 5 6 7 8 9 10

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)


Gregory Morrisett (no lecture notes)

Hardware Verification

Paul Jackson (lecture notes available in 506)