ラムダ・キューブ
Lambda Cube
原点の単純型付きラムダ計算から、Calculus of Constructionsを導く
ラムダ・キューブをさらに一般化したものとして純粋型システムがある
対応
原点
\lambda_\to: 単純型付きラムダ計算
基礎的な抽象化
\lambda2: System F
型に依存した値
依存型をあつかう
値に依存した型
\lambda\underline{\omega}: 高階多相型
型に依存した型
kindなどを扱う
組み合わせたもの
\lambda P\underline{\omega}
ここってあまりないのかな
wikiや本にもあまり書かれていない
\lambda\omega: System Fω
全部入り
\lambda P\omega: Calculus of Constructions
\lambda Cとも書く
関連
参考
龍田『型理論』 8章