- Peter Dybjer and Erik Palmgren, Intuitionistic Type Theory, article to appear in Stanford Encyclopedia of Philosohpy (2015).
- 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)

- My papers on the syntax and semantics of inductive and inductive-recursive definitions
- My paper and talk on generic programming in dependent type theory (the talk is recommended reading!)