Mathematical formalism for expressing computation via function abstraction and application. Equivalent in expressive power to Turing machines and to general/partially recursive functions — one can always be translated into another. Cited in Halasz's talk as one of the ways to describe recursively enumerable languages and as an equivalent formulation of the Church-Turing thesis.