设 $𝑡$ 是 词项的集合 中的词项． 类型的语法为 $𝑇⩴\text{ Bool }|\text{ Nat}$，分别表示布尔类型与自然数类型． 词项与类型是不同的语法类别，类型系统定义的是它们之间的关系．

类型关系由下面七条类型规则归纳定义：它是对这些规则封闭的最小关系． 类型判断 $⊢𝑡:𝑇$ 读作“可以由类型规则推出词项 $𝑡$ 具有类型 $𝑇$”； 判断成立，当且仅当存在以它为结论的有限推导．

推导符号 $⊢$ 属于元语言，用来标记可推导性，与词项构造子或求值符号无关． 含变量的语言通常写作 $\mathrm{\Gamma }⊢𝑡:𝑇$， 读作“在语境 $\mathrm{\Gamma }$ 中，词项 $𝑡$ 具有类型 $𝑇$”． $\mathrm{\Gamma }$ 也称类型环境，记录作用域内变量的类型假设； $⊢$ 把这些假设与待证陈述分开． 词项的集合 的算术语言没有变量，所以采用空语境，并省略 $\mathrm{\Gamma }$． 为简洁起见，讨论这套规则时，$𝑡:𝑇$ 是 $⊢𝑡:𝑇$ 的简写．

横线上的判断是前提，横线下的是结论； 没有前提的规则称为公理，仍是推导规则的特例． $𝑇$、${𝑡}_1$ 等符号按 元变量 代换： $𝑇$ 只能取类型，${𝑡}_1$ 只能取词项； T-If 两个分支里的 $𝑇$ 必须代换成同一个类型．