Simply typed lambda calculus

The simply typed lambda calculus is the lambda calculus with a type system that assigns every term a type and restricts application to well-typed combinations. Invented by Alonzo Church in 1940 as a response to the paradoxes of the untyped system, it forfeits the universality of the untyped calculus — not every computable function is expressible — in exchange for a guarantee that every well-typed program terminates. This trade-off between expressiveness and safety is the template for every modern programming language type system.

The simply typed lambda calculus is the computational face of intuitionistic propositional logic under the Curry-Howard correspondence. A type is a proposition; a well-typed term is a proof; beta reduction is proof normalization. This identity makes the simply typed lambda calculus the simplest system in which proof and computation are the same activity. Its extensions — polymorphic types, dependent types, linear types — have become the foundational languages of formal verification. The fact that type discipline prevents the construction of a fixed-point combinator is not a limitation but a feature: it draws a precise boundary between total and partial computation, between programs that always halt and programs that might not. The generalization that restores expressiveness while retaining type safety is the polymorphic lambda calculus — most famously, Girard's System F.