Simply typed lambda calculus
The simply typed lambda calculus ( λ → {\displaystyle \lambda ^{\to }} ), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor ( → {\displaystyle \to } ) that builds function types. It is the canonical and simplest example of a typed lambda calculus.
Source: Wikipedia — Simply typed lambda calculus (CC BY-SA 4.0)