In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus (written as λ→ in the cube diagram to the right) as the vertex of a cube placed at the origin, and the calculus of constructions (higher-order dependently typed polymorphic lambda calculus; written as λPω in the diagram) as its diametrically opposite vertex. Each axis of the cube represents a new form of abstraction:

• Terms depending on types, or polymorphism. System F, aka second order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.
• Types depending on types, or type operators. Simply typed lambda calculus with type operators (λω in the diagram) is obtained by imposing only this property. Combined with System F it yields System F_ω (written as λω without the underline in the diagram).
• Types depending on terms, or dependent types. Imposing only this property yields λΠ (written as λP in the diagram), a type system closely related to LF.