Intuitionistic type theory (or Martin-Löf’s type theory, the two names are interchangeable) is a foundation for constructive mathematics and computer programming.
Unfortunately, intuitionistic type theory does not yet have any authoritative presentation and many important works are either out of print or otherwise not readily available. The purpose of the following listing is to make some important books and articles available to the interested public.
Works by Martin-Löf
- 1982. “Constructive mathematics and computer programming” (PDF). This important paper was written after the Padua lectures, published in book Intuitionistic Type Theory (cf. infra), were held (1980). It explains how type theory can be viewed as a programming language.
- 1984. Intuitionistic Type Theory (PDF), Bibliopolis. This is the book on Martin-Löf’s type theory. The rules for propositional equality (pp. 59-64) have been withdrawn, but otherwise it stands the test of time. I can but warmly recommend this book. With due permission from the author, I have the privilege of making this book available in PDF format. (Thanks to Johan Glimming for scanning the book.)
- 1996. “On the meaning of the logical constants and the justifications of the logical laws“. In this series of lectures, Per Martin-Löf explains the philosophy behind his intuitionistic type theory. These notes are indispensible to the serious student of Martin-Löf’s type theory.
- 2006. “100 years of Zermelo’s axiom: what was the problem with it?” (Oxford Journals, login required). This is the latest published work by Per Martin-Löf, in which he shows that the problem with the axiom of choice is not choice, but extensionality of choice.
Works by other authors
- J. G. Granström. Treatise on Intuitionistic Type Theory (2011). An improved version of the below doctoral thesis.
- J. G. Granström. Reference and Computation in Intuitionistic Type Theory (PDF). The doctoral thesis of the author of this page. It contains several references to works relevant to the study of Martin-Löf’s type theory.
- B. Nordström, et al. “Martin-Löf’s Type Theory” (PDF). This chapter from the handbook of logic in computer science (vol. 5, 2001) is, to date, the most authoritative presentation of Martin-Löf’s type theory. It differs somewhat in scope and contents from Martin-Löf’s 1984 book: the rules for propositional equality are corrected and the higher type structure is included. However, the meaning explanations for the higher type structure are not the ones given by Martin-Löf.
- B. Nordström, et al. Programming in Martin-Löf’s Type Theory (PDF). This is an out of print book published by Oxford University Press in 1990. This electronic copy of the book seems to be free.
- T. Streicher. Investigations Into Intensional Type Theory (PDF). Streicher’s Habilitationsschrift from 1993 contains a wealth of detailed type-theoretic derivations.
- S. Valentini. “Another introduction to Martin-Löf ’s Intuitionistic Type Theory” (PDF). Published in “Trends in Theoretical Informatics”, 1996.