¶ 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 λ-calculus, and the way it applies to the study of programming languages.
- Introduction
- 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
- Normalization
- References
- Exceptions
-
Subtyping
- Subtyping
- Metatheory of Subtyping
- An ML Implementaiton 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