Abstract Interpretation and Galois Connections
Sound approximation, made rigorous. The principled answer to the tradeoff Rice's theorem forces on you.
Pl-Theory
Parametricity: Theorems for Free
A polymorphic type alone tells you what the function must do. can only permute.
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.
The Lambda Calculus and the Y Combinator
Three rules, all of computation, and recursion built from nothing. Absorbs Church–Rosser confluence: reduction order doesn't change the answer.
The CALM Theorem and CRDTs
A program can be coordination-free iff it's monotone. The positive result hiding behind all the impossibility ones.
Rice's Theorem
Every non-trivial semantic property of programs is undecidable.