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.