Dependent type theory and proof assistants - introduction and overviews

• Dependent Types at Work (with Ana Bove), lecture notes from the LerNET Summer School, Piriapolis, February 2008.
• A Brief Overview of Agda - A Functional Language with Dependent Types (with Ana Bove and Ulf Norell), in Proceedings of TPHOLs 2009, Munich.

• 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.