Cálculo lambda
Modelo formal de computação, criado por Alonzo Church nos anos 1930. Três regras básicas: variáveis, abstração (λx.corpo) e aplicação (f x). É Turing-completo — calcula tudo o que um computador calcula.
Base da programação funcional. O currying (funções de um único argumento que devolvem outras funções) leva o nome de Haskell Curry. O combinador Y permite recursão sem funções nomeadas. Os cálculos lambda tipados (Simply Typed → System F → Cálculo das Construções) levaram a Haskell, ML, Coq, Agda e Lean; a programação funcional é herança direta. A tese de Church-Turing diz que o cálculo lambda e as máquinas de Turing expressam a mesma classe computacional.