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}
Here are the slides of my lectures at the Proofs as Programs Summer School in Eugene Oregon, June-July 2002:
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):