Types and Programming Languages (ISBN:0262162091) by BenjaminPierce. Quite simply the most comprehensive work on TypeTheory that currently exists today. Highly technical, and likely a bit difficult for laymen to grasp, but covers the subject in great depth and breadth. Contains lots of important introductory material, such as a thorough introduction to the LambdaCalculus.
http://www.cis.upenn.edu/~bcpierce/tapl/
Followed by AdvancedTopicsInTypesAndProgrammingLanguages.