Types and Programming Languages (TAPL)

A seminal PL theory book by Benjamin C. Pierce. It is often affectionately referred to as TAPL.

First and foremost, TAPL is the quintessential textbook introduction to typed \lambda-calculus, and the way it applies to the study of programming languages.

Table of contents (pdf)

1. Introduction
2. Mathematical Preliminaries

• Untyped Systems

  3. Untyped Arithmetic Expressions
  4. An ML Implementation of Arithmetic Expressions
  5. The Untyped Lambda-Calculus
  6. Nameless Representation of Terms
  7. An ML Implementation of the Lambda-Calculus

• Simple Types

  8. Typed Arithmetic Expressions
  9. Simply Typed Lambda-Calculus
  10. An ML Implementation of Simple Types
  11. Simple Extensions
  12. Normalization
  13. References
  14. Exceptions

• Subtyping

  15. Subtyping
  16. Metatheory of Subtyping
  17. An ML Implementaiton of Subtyping
  18. Case Study: Imperative Objects
  19. Case Study: Featherweight Java

• Recursive Types

  20. Recursive Types
  21. Metatheory of Recursive Types

• Polymorphism

  22. Type Reconstruction
  23. Universal Types
  24. Existential Types
  25. An ML Implementation of System F
  26. Bounded Quantification
  27. Case Study: Imperative Objects, Redux
  28. Metatheory of Bounded Quantification

• Higher-Order Systems

  29. Type Operators and Kinding
  30. Higher-Order Polymorphism
  31. Higher-Order Subtyping
  32. Case Study: Purely Functional Objects

Links

• Official book website.

• How often do books have their own Wikipedia page?