Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.