型理論において、ラムダ・キューブ () とは、8つの異なる型付きラムダ計算の関係を表した図である。これらの計算体系がそれぞれ型（type）と項（term）の間にどのような依存関係を認めるかを整理したもので、単純型付きラムダ計算から、を導くフレームワークになっている。数学者ヘンク・バレンドレヒトによって1991年に提唱された。
（右図参照）ラムダキューブの原点は、単純型付きラムダ計算に相当する。三つの座標軸は、Y軸=パラメトリック多相、Z軸=型オペレータ、X軸=依存型に対応している。X, Y, Zの三軸線を融合した終点のは、Calculus of Constructionsに相当する。
各頂点は、以下の通りである: λ→ 項に依存した項（単純型付きラムダ計算） 一階命題論理 （これを以下全てが含む。） λ2 型に依存した項（System F） パラメトリック多相 二階命題論理 λ 型に依存した型（System F） 型オペレータ 弱性高階命題論理 λω 型に依存した型、型に依存した項（System Fω） 型構築子 高階命題論理 λ2とλの融合 λP 項に依存した型（） 依存型 一階述語論理 λP2 型に依存した項、項に依存した型（） 依存型 二階述語論理 λPとλ2の融合 λP 項に依存した型、型に依存した型（） 依存型 弱性高階述語論理 λPとλの融合 λC 型に依存した型、型に依存した項、項に依存した型（） CoC 高階述語論理 λP2とλPの融合
参考文献