Thanks, added to the bookmarks. Alongside with the one I found earlier http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf, this book seem to cover not the type theory per se, but the mathematics that make its foundations. This is great, though not exactly what I'm looking for.
It depends what you mean by "type theory", but you're right. See Pierce for a more practical introduction. "Proofs and Types" is more fundamental and focuses on the interplay between the operational semantics of the underlying language and the structure of its type system (read as proofs of properties of programs written in the language).
