Rachunek lambda
Formalny model obliczeń. Alonzo Church, lata 30. XX wieku. Trzy reguły: zmienne, abstrakcja (λx.ciało) i aplikacja (f x). Jest Turing-zupełny — policzy wszystko, co potrafi komputer.
Fundament programowania funkcyjnego. Currying (funkcje jednego argumentu zwracające kolejne funkcje) nazwano od Haskella Curry'ego. Kombinator Y pozwala na rekurencję bez nazwanych funkcji. Typowane rachunki lambda (proste typy → System F → rachunek konstrukcji) doprowadziły do Haskella, ML, Coqa, Agdy i Leana. Programowanie funkcyjne to bezpośredni spadek po nim. Teza Churcha-Turinga mówi, że rachunek lambda i maszyny Turinga wyrażają tę samą klasę obliczeń.