Why did lambda calculus see widespread use in programming language specification, type system studies, etc?

• Mid 1960, Peter Landin observed that a complex programming language can be understood by:

  • The formulation of the language as a tiny core calculus capturing the language's essential mechanisms.

  • Together with a collection of convenient derived forms whose behavior is understood by translating them into the core.

    [Landin, 1964, 1965, 1966; Tennent, 1981]

• The core language used by Landin was the lambda-calculus, a formal system invented in the 1920s by [Alonzo Church, 1936, 1941], in which all computation is

reduced to the basic operations of function definition and application.

• Following Landin's insight, as well as the pioneering work on Lisp [John McCarthy, 1959, 1981], the lambda-calculus has seen widespread use in many areas.

  • The specification of programming language features.

  • Language design.

  • Language implementation.

  • The study of type systems.