Editing Lambda cube (section)

=== (λP) Lambda-P ===
In the [[λΠ-calculus|λP]] system, also named λΠ, and closely related to the [[Logical framework#LF|LF Logical Framework]], one has so called [[dependent types]]. These are ''types that are allowed to depend on terms''. The crucial introduction rule of the system is

<math>\frac{\Gamma, x : A \;\vdash\; B : *}{\Gamma \;\vdash\; (\Pi x : A . B) : *}</math>

where <math>*</math> represents valid types. The new type constructor <math>\Pi</math> corresponds via the [[Curry Howard isomorphism|Curry-Howard isomorphism]] to a universal quantifier, and the system λP as a whole corresponds to [[first-order logic]] with implication as only connective. An example of these dependent types in concrete programming is the type of vectors on a certain length: the length is a term, on which the type depends.