Dependent type theory and proof assistants - introduction and overviews
- Dependent Types in Programming, lectures for
the TYPES Summer School, Giens, France, September 2002.
- Constructive Type Theory and Interactive Theorem Proving, invited lecture at 22nd JSSST, Sendai, Japan, September 2005.
- History of the Identity Type, talk at the Workshop on Identity Types - Topological and Categorical Structure, Uppsala, November 2006.