The simply typed lambda calculus adds types to lambda abstractions and applications so that impossible function uses are rejected statically.

Types are built from base types and function types:

$$T ::= \text{Bool}\mid\text{Int}\mid T\to T.$$

An abstraction can annotate its parameter:

$$\lambda x:T_1.e.$$

If the body has type $T_2$ assuming $x:T_1$, then the function has type $T_1\to T_2$:

$$\frac{\Gamma,x:T_1\vdash e:T_2} {\Gamma\vdash \lambda x:T_1.e:T_1\to T_2}.$$

Application requires the argument type to match the function's input type:

$$\frac{\Gamma\vdash e_1:T_1\to T_2\qquad \Gamma\vdash e_2:T_1} {\Gamma\vdash e_1\ e_2:T_2}.$$

Thus

$$(\lambda x:\text{Int}.x+1)\ 4$$

is well typed, while applying the same function to a Boolean is rejected.

Simple types rule out self-application such as $x\ x$ when $x$ would need simultaneously to be both an argument and a function of itself. As a consequence, the pure simply typed lambda calculus is strongly normalizing: every well-typed term terminates.

This small calculus is a laboratory for understanding function types, static checking and type-safety proofs before adding polymorphism, subtyping, state or effects.