**MRI masterclass (Spring 2003)**

The slides are the ones from the Eugene Summer School (see below),
apart from the Inductive Types slides that have been added in the list
hereunder.

Exercises of the MRI masterclass are listed here. Some are Coq .v
files and others are .ps.gz files 2003).

BTW: To run Coq
with XEmacs and Proof General from your account, it should be enough
to put this line last in your .bashrc:

export
PATH=/vol/s1studio/ee/bin:${PATH}

- Simple Type Theory Exercises,
- Coq .v file with Simple Type Theory Exercises,
- Coq .v file with the answers to the Simple Type Theory Exercises,
- Polymorphic Type Theory Exercises.
- ps.gz file with the answers to the Polymorphic Type Theory Exercises,
- Coq .v file with Dependent Type Theory Exercises,
- Coq .v file with the answers to the Dependent Type Theory Exercises.
- Higher Order Logic Exercises, the .ps.gz file,
- Higher Order Logic Exercises, the .v file,
- Slides of Lecture 6 (Inductive Types) ,
- Coq .v file for Lecture 6 (Inductive Types) .
- Record Types Exercises, a .v file.

Here are the slides of my lectures at the **Proofs as Programs Summer
School in Eugene Oregon**, June-July 2002:

- Simple Type Theory ,
- Polymorphic Type Theory,
- Dependent type theory/ Logical Framework,
- Higher Order Logic,
- Pure Type Systems,
- Various Type Theoretic Topics,
- Fundamental Theorem of Algebra in Coq.

Here are the slides of my lectures at the **Types Summer School in
Giens, France**, September 2002 (most of it is a condensation of the
ones of Eugene):

Slides of my lectures at the **Calculemus Autumn School in Pisa, Italy**,
September-October 2002 (a different condensation of the slides of
Eugene, with a Coq source file to illustrate):

- Type Theory for Formalizing Maths ,
- Coq source file with illustrations,
- Formalization of FTA in Coq.

herman Last modified: Mon Mar 27 11:34:38 CEST 2006