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