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