A
typed lambda calculus is a typed
formalism that uses the lambda-symbol (
?) to denote anonymous function abstraction. Typed lambda calculi are foundational
programming languages and are the base of typed
functional programming languages such as
ML and
Haskell and, more indirectly, typed
imperative programming languages. They are closely related to
mathematical logic and
proof theory via the
Curry-Howard isomorphism and they can be considered as the internal language of classes of
categories, e.g. the simply typed lambda calculus is the language of
Cartesian closed categories (CCCs).
From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type.
Various typed lambda calculi have been studied The types of the simply typed lambda calculus are only base types (or type variables) and function types 
. 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. System F allows polymorphism by using universal quantification over all types; from a logical perspective it can describe all functions which are provably total in second-order logic. Lambda calculi with dependent types are the base of intuitionistic type theory, the calculus of constructions and the logical framework (LF), a pure lambda calculus with dependent types. Based on work by Berardi, 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).
Some typed lambda calculi introduce a notion of subtyping, i.e. if A is a subtype of B, then all terms of type A also have type B. Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and 
(F-sub).
