# 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)