- 項と型の型付け〈typing〉チェック ＝ 証明と命題の演繹〈deduction〉チェック
- 型付けの宣言〈型宣言 | 型判断〉 ＝ 演繹の宣言〈命題判断〉 ＝ 無名定理
- 型付けの正しさ〈correctness〉＝ 演繹〈deduction〉の正しさ
- 項の型 ＝ 証明の結論命題〈ターゲット命題〉
- 項のコンテキスト〈型コンテキスト | 型付けコンテキスト〉 ＝ 証明のコンテキスト〈命題コンテキスト | 演繹コンテキスト〉
- 項の型推論：項の戻り型〈return type〉を推論する ＝ 証明の結論推論：証明のターゲット命題〈結論〉を推論する
- 関数の戻り型 ＝ 定理の結論〈ターゲット〉命題
- 関数の引数型 ＝ 定理の前提命題
- hypothesis はコンテキストの意味と、コンテキストに入れられる公理の意味もある。
- goal はパターン変数を持つシーケント＝質問＝問題 の意味もあるし、ターゲット命題のこともある。
記法は：
- $`\Gamma \vdash t : X`$ 型コンテキストのもとでの、項の型付け宣言、全体として型判断
- $`\Gamma \mid \Theta \vdash p : A`$ 型コンテキストと命題コンテキストのもとでの、証明項の演繹宣言、全体として命題判断
- $`\Gamma \vdash X`$ 型の在住性〈inhabited-ness〉判断＝集合の非空性判断
- $`\Gamma \mid \Theta \vdash A`$ 命題の在住性判断＝構成的証明可能性判断
