| 型理論 | 論理 |
|---|---|
| 集合圏 Set | 論理圏 Logic |
| 型のポイントインスタンス | 命題の証拠 |
| 引数リスト | 前提〈仮定 | 仮説〉リスト |
| 関数 | 定理 |
| 戻り値型 | 結論命題 |
| 関数の計算 | 定理の証明 |
| 関数のプロファイル | 定理のステートメント |
| トップダウン関数定義 | バックワード・リーズニング |
| ボトムアップ関数定義 | フォワード・リーズニング |
| ラムダ計算 | 自然演繹 |
| コンビネータ計算 | シーケント計算 |
| 関数コンビネータ | リーズニング規則 |
| 関数の定義行為 | 定理の証明行為 |
| プログラミング | 証明行為 |
| プログラムコード | 証明コード〈項 | スコア | 譜〉 |
| 関数の本体コード | 定理の本体コード〈項 | スコア | 譜〉 |
| 計算項〈コード | 項〉 | 証明項 |
| 関数ライブラリ | 定理ライブラリ |
| マルチチャネル出力（典型的には例外） | 選言結論 |
| 引数 | 明示的前提 |
| 環境 | 暗黙の前提 |
