Typed lambda calculus

${\displaystyle \lambda }$

Various typed lambda calculi have been studied. The simply typed lambda calculus has only one type constructor, the arrow ${\displaystyle \to }$, and its only types are

${\displaystyle \sigma \to \tau }$.

Some typed lambda calculi introduce a notion of subtyping, i.e. if ${\displaystyle A}$ is a subtype of ${\displaystyle B}$, then all terms of type ${\displaystyle A}$ also have type ${\displaystyle B}$. Typed lambda calculi with subtyping are the simply typed lambda calculus with conjunctive types and

All the systems mentioned so far, with the exception of the untyped lambda calculus, are