単純型付きラムダ計算

型を、基本型 $o_1,o_2,\ldots$ から $A\to B$ で作られるものとする（$\to$ は右結合）。項は型なしの λ 項と同じだが、抽象に束縛変数の型を書いて $\lambda x{:}A.M$ とする。文脈 $\Gamma$ は変数と型の組 $x_1{:}A_1,\ldots,x_n{:}A_n$ の有限列（変数は相異なる）で、型付け判断 $\Gamma\vdash M:A$ を次の 3 規則で帰納的に定める。

β 簡約 $(\lambda x{:}A.M)N\to_\beta M[x:=N]$ と置換は型なしの場合と同じに定める。