Parametricity: Theorems for Free
A polymorphic type alone tells you what the function must do. can only permute.
Type-Theory
Progress and Preservation
"Well-typed programs don't go wrong", stated as the two lemmas that actually prove it. What a type system does and does not promise.
Hindley–Milner and Principal Types
Every typable term has one most general type, and it's inferable. Why ML and Haskell need so few annotations, and why subtyping breaks it.
The Curry–Howard Correspondence
Programs are proofs, types are propositions, evaluation is proof simplification. The most beautiful idea in the series.