MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am interested in learning the theory of types, especially in how they can provide a foundation to mathematics different to sets and how they can avoid self-referential paradoxes by stipulating that a collection of objects of type n has type n+1. As for my background knowledge, I only know a little of propositional and predicate logic and Zermelo-Fraenkel set theory.

share|cite|improve this question
up vote 11 down vote accepted

I would suggest you look at Martin-Löf's work, such as the following reprint of his earlier unpublished manuscript (from 1972?):

  • Per Martin-L: An Intuitionistic Theory of Types. In: Twenty-Five Years of Constructive Type Theory Proceedings of a Congress held in Venice, October 1995. Editors: Giovanni Sambin and Jan M. Smith. Oxford University Press, 1998.

I belive a fairly good approximation of this paper is available online. If you are looking for other online references, have a look at this lecture by Martin-Löf.

This should give you some idea for type theory as foundation of mathematics.

share|cite|improve this answer

The kind of type theory you're asking about, Russell's simple theory of types, is from about the early 1900's. Here's a reference:

  • Russell, Bertrand: Mathematical Logic as Based on the Theory of Types. Amer. J. Math. 30 (1908), no. 3, 222--262.

Recent work in type theory is somewhat different, continuing the tradition of Per Martin-Löf. In addition to his work (referenced by Andrej), I would also recommend the following book by Luo:

  • Luo, Zhaohui: Computation and reasoning. A type theory for computer science. International Series of Monographs on Computer Science, 11. The Clarendon Press, Oxford University Press, New York, 1994. xii+228 pp. ISBN: 0-19-853835-9.

For the relation between set theory, type theory, and category theory, you might want to have a look at this preprint by Steve Awodey.

There's also an n-lab page, and the type theory page at Stanford Encyclopedia of Philosophy has a reference section.

share|cite|improve this answer

In terms of modern type theory, you might be best off playing around with Coq; this will give you instant feedback on any misconceptions you might have about how things work. The book Coq'Art (linked from the Coq website) is quite good and the system hasn't changed too much since the book was written.

share|cite|improve this answer

I found this a valuable and concise introduction:

The Seven Virtues of Simple Type Theory by William M. Farmer.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.