対象物：
- 型
- 関数
- 値〈データ | ポイント〉 特別な関数
- 汎関数〈メタ関数〉
- 命題（真偽値、述語、論理式）
- 導出
- 保証 特別な導出
- リーズニング〈メタ導出〉
カリー／ハワード／ランベック対応
| 型 | 命題 |
| 関数 | 導出 |
| 値 | 保証 |
| 汎関数 | リーズニング |
項：
- 型項（多くの場合は集合項）
- 関数項〈項〉
- 値項
- 汎関数項
- 命題項〈論理式〉
- 導出項〈証明項〉
- 保証項
- リーズニング項
バンチと書き換えアクション：
- 型バンチと型構成子〈型コネクティブ〉
- 関数バンチと関数構成子〈関数コネクティブ〉
- 値バンチと値構成子〈値コネクティブ〉＝関数後結合主体
- 汎関数バンチと汎関数構成子〈汎関数コネクティブ〉
- 命題バンチと命題構成子〈論理コネクティブ〉
- 導出バンチと導出構成子〈導出コネクティブ〉
- 保証バンチと保証構成子〈保証コネクティブ〉＝導出後結合＋リーズニング
- リーズニングバンチとリーズニング構成子〈リーズニングコネクティブ〉
構成スクリプト：
- 型構成スクリプト
- 関数構成スクリプト＝汎関数スクリプト
- 値構成スクリプト＝関数スクリプト
- 汎関数構成スクリプト
- 命題構成スクリプト＝導出スクリプト
- 導出構成スクリプト＝リーズニング・スクリプト
- 保証構成スクリプト＝導出スクリプト？
課題：スクリプトレベルでのカリー／ハワード／ランベック対応
