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. 



Reference request for type theory
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](http://books.google.si/books?id=pLnKggT_In4C&printsec=frontcover&hl=en&source=gbs_v2_summary_r&cad=0#v=onepage&q=&f=false). 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](http://www.cs.chalmers.se/~peterd/kurser/tt03/martinlof72.ps). If you are looking for other online references, have a look at [this lecture by Martin-Löf](http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.html).


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


