In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below).
Typed lambda calculi are closely related to mathematical logic and proof theory via the Curry–Howard isomorphism and they can be considered as the internal language of certain classes of categories.
System T extends the simply typed lambda calculus with a type of natural numbers and higher-order primitive recursion; in this system all functions provably recursive in Peano arithmetic are definable.
Based on work by Berardi on pure type systems, Henk Barendregt proposed the Lambda cube to systematize the relations of pure typed lambda calculi (including simply typed lambda calculus, System F, LF and the calculus of constructions).
[3] Some typed lambda calculi introduce a notion of subtyping, i.e. if
All the systems mentioned so far, with the exception of the untyped lambda calculus, are strongly normalizing: all computations terminate.
Systems with explicit recursion combinators, such as Plotkin's "Programming language for Computable Functions" (PCF), are not normalizing, but they are not intended to be interpreted as a logic.
In computer programming, the routines (functions, procedures, methods) of strongly typed programming languages closely correspond to typed lambda expressions.