λ-立方。箭头的方向展示了包含关系。 在数理逻辑 和类型论 中，λ-立方 是探索 Coquand 的构造演算 中细化轴的框架，以简单类型 λ-演算 （在立方图中写作 λ→）作为原点放在立方体的顶点，而构造演算（即高阶依赖类型化 λ-演算，在图中写作 λPω）则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式：
值依赖类型，或多态 。系统F ，即二阶λ-演算（图中写作 λ2）就是通过只加入此性质得到的。
类型依赖类型，或类型构造器 。带类型构造器的简单类型 λ-演算 （图中为
λ λ -->
ω ω -->
_ _ -->
{\displaystyle \lambda {\underline {\omega }}}
系统F 结合就产生了系统Fω（在图中写作不带下划线的λω）。
类型依赖值，或依赖类型 。只加入此性质就得到了λΠ （在图中写作λP），一种与LF 紧密相关的类型系统。 所有的八种演算包含了最基本的抽象形式，值依赖值即简单类型 λ-演算 中的普通函数。此立方中最丰富的演算即构造演算 ，它带有所有三种抽象。所有八种演算都是强规范化 的。
然而子类型 并未展示在此立方中，尽管像
F
<:
ω ω -->
{\displaystyle F_{<:}^{\omega }}
高阶有界量化 闻名的，结合了子类型和多态的系统具有实际意义，它可被进一步推广为有界类型构造器 。进一步扩展到
F
<:
ω ω -->
{\displaystyle F_{<:}^{\omega }}
纯函数对象 的定义；这些系统通常在λ-立方的论文发表后才被开发出来。
F
<:
ω ω -->
{\displaystyle F_{<:}^{\omega }}
[ 1]
此立方的思想来源于Henk Barendregt (1991)。就此立方的所有角而言，纯类型系统 的框架涵盖了λ-立方，其它一些系统也可表示为此通用框架的实例。[ 2]
Olivier Ridoux 在他的 Habilitation à diriger les recherches Lambda-Prolog de A à Z... ou presque 中给出了此立方的一个截边角后的模版(p. 70) 的两种表示，一种将此立方表示为一个八面体，其中 8 个顶点以面代替，另一种将它表示为一个十二面体，其中 12 条棱则以面代替。
Some of the systems included in the cube were first defined in Automath.
同伦类型论
^ Pierce, 2002, chapters 31 and 32
^ Pierce, 2002, p. 466
