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}}