采用 类型与类型判断 的类型关系、 多步规约 的运行关系， 以及 正规形式与受阻 的受阻判定． 称这套语言规则具有类型安全性，如果对任意词项 $𝑡$、${𝑡}^{\prime }$ 和类型 $𝑇$： 若 $𝑡:𝑇$ 且 $𝑡{⟶}^{\ast }{𝑡}^{\prime }$，则 ${𝑡}^{\prime }$ 没有受阻．

这个性质表达了类型规则相对于执行规则的类型健全性： 良类型词项的执行不会进入所定义的错误状态． 它不直接涉及某个具体检查算法，也不承诺终止或排除真实语言中的所有运行时错误．