Lambda cube
901593
222525244
2008-06-29T20:31:21Z
Alaibot
1324179
Robot: sorting stub (based on existing categorisation)
In [[mathematical logic]] and [[type theory]], the '''λ-cube''' is a framework for exploring the axes of refinement in [[Thierry Coquand|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 (computer science)|polymorphism]] (as in [[System F]]),
* Types depending on types, or type operators, and
* Types depending on terms, or [[Dependent type theory|dependent types]] (as in [[LF (logical framework)|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 [[Normalization property (lambda-calculus) |strongly normalizing]].
The idea of the cube is due to the mathematician [[Henk Barendregt]] (1991).
==See also==
* [[Lambda calculus]]
* [[System F]]
==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. [http://citeseer.ist.psu.edu/peytonjones97henk.html ''Henk: A Typed Intermediate Language'']
* [http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm Barendregt's Lambda Cube]
[[Category:Lambda calculus]]
{{formalmethods-stub}}