Pierce Benjamin C. Types and Programming Languages

Cambridge/Massachusetts (USA), London/England: The MIT Press, 2002. — 645 p.The study of type systems—and of programming languages from a type-theoretic perspective—has become an energetic field with major applications in software engineering, language design, high-performance compiler implementation, and security. This text offers a comprehensive introduction to the fundamental definitions, results, and techniques in the area.Mathematical Preliminaries
Untyped Systems
Untyped Arithmetic Expressions
An ML Implementation of Arithmetic Expressions
The Untyped Lambda-Calculus
Nameless Representation of Terms
An ML Implementation of the Lambda-Calculus
Simple Types
Typed Arithmetic Expressions
Simply Typed Lambda-Calculus
An ML Implementation of Simple Types
Simple Extensions
NormalizationExceptions
Subtyping
Subtyping
Metatheory of Subtyping
An ML Implementation of Subtyping
Case Study: Imperative Objects
Case Study: Featherweight Java
Recursive Types
Recursive Types
Metatheory of Recursive Types
Polymorphism
Type Reconstruction
Universal Types
Existential Types
An ML Implementation of System F
Bounded Quantification
Case Study: Imperative Objects, Redux
Metatheory of Bounded Quantification
Higher-Order Systems
Type Operators and Kinding
Higher-Order Polymorphism
Higher-Order Subtyping
Case Study: Purely Functional Objects
Appendices
Solutions to Selected Exercises
Notational Conventions