Lambda cube

From Wikipedia, the free encyclopedia

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 as the vertex of a cube placed at the origin, and the calculus of constructions (higher order dependently-typed polymorphic lambda calculus) as its diametric opposite vertex. Each axis of the cube represents a new form of abstraction:

• Terms depending on types, or polymorphism (as in System F),
• Types depending on types, or type operators, and
• Types depending on terms, or dependent types (as in LF).

All eight calculi include the most basic form of abstraction, terms depending on terms, ordinary functions as in the simply-typed lambda calculus.

All eight calculi are strongly normalizing.

The idea of the cube is due to the mathematician Henk Barendregt (1991).

[edit] See also

• Lambda calculus
• System F

[edit] References

• H.P. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, 1(2):125-154, April 1991.
• Simon Peyton Jones and Erik Meijer, 1997. Henk: A Typed Intermediate Language
• Barendregt's Lambda Cube