Pierce's Types and Programming Languages is a masterful introduction to the theory and practice of type systems. One of the things that makes this book so great is that it is equally accessible to both the theory-oriented and the practice-oriented. This was driven home to me in a conversation with Ola Bini, when I saw he was carrying this book, and he commented "I love this book because I can skip all the math and get what I need from the ML implementation." I answered that I liked it for the opposite reason; I was able to get everything I needed from the math and didn't have to look at the code. Its pretty impressive that a book can be that useful and successful from two such radically different reader approaches.
I found that Pierce's treatment was extremely accessible. He starts with almost no assumptions, introduces first the untyped lambda calculus, then the simply typed lambda calculus, some obvious extensions (records, references, subtyping, union types, functional objects, etc), operational semantics, and builds gradually to more useful type systems. Each section includes motivation, analysis, a formal description of the system, soundness proofs, and ML code; the impatient can skip some of these and still get what he's talking about. There is working code for each of the languages developed. (The type systems were developed in a system that the author wrote called TinkerType, which makes it possible to build type systems by "mixing and matching" features, and it generates both the ML code and TeX source for generating the figures used in the book -- most impressive!)
Not only is this book useful to anyone who is interested in the design and science of programming languages, but it is also a pleasure to read.
What's your favorite computer science book? (Unoriginality points for anyone who says TAOCP.)
