- Peter Dybjer and Erik Palmgren, Intuitionistic Type Theory, Stanford Encyclopedia of Philosohpy (2016).
- Per Martin-Löf, An Intuitionistic Theory of Types (1972)
- Per Martin-Löf, Constructive Mathematics and Computer Programming (LMPS 1979)
- Per Martin-Löf, Intuitionistic Type Theory (Bibliopolis 1984)

- An Introduction to Programming and Proving in Agda, Jan 2018
- My papers on the syntax and semantics of inductive and inductive-recursive definitions
- My paper and talk on generic programming in dependent type theory