🔬 Discovery

Lambda calculus

Cálculo lambda

Date
1932-1936 · confidence high
Place
Princeton, New Jersey, United States
Credited to
Alonzo Church
Field
Knowledge & symbols

What was discovered

American logician Alonzo Church introduced at Princeton, between 1932 and 1936, lambda calculus, a formal system for expressing functions and their application through abstraction and substitution, originally conceived within a broader program on the foundations of mathematical logic.

The original 1932-1933 system turned out to be logically inconsistent (the Kleene-Rosser paradox, 1935); in 1936 Church isolated and published the portion relevant to computation, now known as the untyped lambda calculus.

What it led to

  • a formalization of computability, shown equivalent to the Turing machine (the Church-Turing thesis)
  • the theoretical foundation of functional programming languages
  • a direct influence on languages such as Lisp and Haskell

Links

Sources✓ verified 2026-09-25