[约定] 元变量 [metavariables]

[定义] 项的集合 [set-of-terms]

[定义] 良类型 [well-typed-terms]

[例] 良类型与不良类型 [well-typed-and-ill-typed-terms]

[约定] 元变量 [metavariables]

[附注] 不完整规格中的类型检查问题 [answers-to-incomplete-specification-questions]

[定理] 进展 [progress]

[定义] 对象语言与元语言 [object-language-and-metalanguage]

[例] 进展 [progress]

[引理] 反演 [typing-inversion]

[附注] 静态类型与动态类型 [static-and-dynamic-typing]

[] 类型：语法导向、反演与唯一性 [typing]

[附注] 显式错误规则与 Kotlin 的底类型 [explicit-errors-and-kotlin-bottom-type]

[附注] 不是所有规则都能直接照抄成算法 [turning-rules-into-algorithms]

[] 回头看与延伸阅读 [summary]

[定义] 可靠与完备 [soundness-and-completeness]

[定义] 类型安全 [type-safety]

[推论] 类型安全 [type-safety]

[附注] 为什么要“对 $𝑇$ 一般化” [generalizing-the-type-in-preservation-proofs]

[附注] Rust 的 ? ? 运算符 [rust-question-mark-operator]

[附注] 类型系统是保守的 [conservative-type-systems]

[定理] 保型 [preservation]

[附注] 反演依赖语法导向 [inversion-and-syntax-directed-rules]

[例] 保型 [preservation]

[定理] 算法可靠性 [type-checking-algorithm-soundness]

[定理] 类型唯一 [uniqueness-of-types]

[附注] Rust 也是元语言 [rust-as-a-metalanguage]

[] 规则与算法：可靠性与完备性 [rules-and-algorithms]

[附注] 从失败的推导里读出错误位置 [locating-errors-in-failed-typing-derivations]

[定理] 算法完备性 [type-checking-algorithm-completeness]

[约定] 阅读约定 [reading-conventions]

[注记] 莱布尼茨与弗雷格 [leibniz-and-frege]

[引理] 典范形式（canonical forms） [canonical-forms]