Lambda-kalkyl
Formell beräkningsmodell. Alonzo Church, 1930-tal. Tre grundregler: variabler, abstraktion (λx.body), applikation (f x). Turing-komplett — kan beräkna allt en dator kan.
Grund för funktionell programmering. Currying (en-argument-funktioner som returnerar andra funktioner) namngavs efter Haskell Curry. Y-kombinator möjliggör rekursion utan namngivna funktioner. Typed lambda calculi (Simply Typed → System F → Calculus of Constructions) ledde till Haskell, ML, Coq, Agda, Lean. Funktionell programmering är direkt arv. Church-Turing-tesen säger att lambda-kalkyl och Turing-maskiner uttrycker samma beräkningsklass.