Lambdacalculus
Formeel rekenmodel van Alonzo Church uit de jaren dertig. Drie basisregels: variabelen, abstractie (λx.body) en applicatie (f x). Turing-volledig: alles wat een computer kan berekenen, kan ook hierin.
De basis van functioneel programmeren. Currying (functies met één argument die andere functies teruggeven) is vernoemd naar Haskell Curry. De Y-combinator maakt recursie zonder benoemde functies mogelijk. Getypeerde lambdacalculi (Simply Typed, System F, Calculus of Constructions) leidden tot Haskell, ML, Coq, Agda en Lean.
Functioneel programmeren is een directe erfenis. Volgens de stelling van Church-Turing drukken lambdacalculus en Turingmachines dezelfde klasse van berekenbaarheid uit.