Simply typed lambda calculus

Definition

Fix a set $B$ of base types and a countable set of variables. The simple types are given by the grammar $\tau ::= b \mid \tau \to \tau$ with $b \in B$. The terms are given by the grammar $t ::= x \mid \lambda x{:}\tau.\, t \mid t\, t$, where $x$ is a variable and $\tau$ is a simple type. A context $\Gamma$ is a finite list $x_1 : \tau_1, \dots, x_n : \tau_n$ of distinct variables with types. The typing relation $\Gamma \vdash t : \tau$ is the least relation closed under these three rules.

1. Variable: if $x : \tau$ occurs in $\Gamma$, then $\Gamma \vdash x : \tau$.
2. Abstraction: if $\Gamma, x : \sigma \vdash t : \tau$, then $\Gamma \vdash (\lambda x{:}\sigma.\, t) : \sigma \to \tau$.
3. Application: if $\Gamma \vdash t : \sigma \to \tau$ and $\Gamma \vdash u : \sigma$, then $\Gamma \vdash t\, u : \tau$.

The simply typed lambda calculus is this typing system together with beta reduction $(\lambda x{:}\sigma.\, t)\, u \to t[u/x]$ on typed terms.