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

0 1 2

## Plastic

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)

## TAL

Gregory Morrisett (no lecture notes)

## Hardware Verification

Paul Jackson (lecture notes available in 506)