Lambda calculus
Formal model of computation. Alonzo Church, 1930s. Three basic rules: variables, abstraction (λx.body), application (f x). Turing-complete — can compute anything a computer can.
Foundation of functional programming. Currying (single-argument functions returning other functions) named after Haskell Curry. The Y combinator enables recursion without named functions. Typed lambda calculi (Simply Typed → System F → Calculus of Constructions) led to Haskell, ML, Coq, Agda, Lean. Functional programming is a direct inheritance. The Church-Turing thesis says lambda calculus and Turing machines express the same computational class.