About Intuitionistic Type Theory

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



Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: