computing point of view, λω is extremely strong, and has been considered as a basis for programming languages. λC The calculus of constructions has both the predicate expressiveness of λP and the computational power of λω, hence why λC is also called λPω, so it is very powerful, both on the logical side and on the computational side. Relation to other systems The system Automath is similar to λ2 from a logical point of view. The ML-like languages, from a typing point of view, lie somewhere between λ→ and λ2, as they admit a restricted kind of polymorphic types, that is the types in prenex normal form. However, because they feature some recursion operators, their computing power is greater than that of λ2. The Coq system is based on an extension of λC with a linear hierarchy of universes, rather than only one untypable , and the ability to construct inductive types. Pure type systems can be seen as a generalization of the cube, with an arbitrary set of sorts, axiom, product and abstraction rules. Conversely, the systems of the lambda cube can be expressed as pure type systems with two sorts , the only axiom , and a set of rules such that . Via the Curry-Howard isomorphism, there is a one-to-one correspondence between the systems in the lambda cube and logical systems, namely: All the logics are implicative (i.e. the only connectives are and ), however one can define other connectives such as or in an impredicative way in second and higher order logics. In the weak higher order logics, there are variables for higher order predicates, but no quantification on those can be done. Common properties All systems in the cube enjoy the Church-Rosser property: if and then there exists such that and ; the subject reduction property: if and then ; the uniqueness of types: if and then . All of these can be proven on generic pure type systems. Any term well-typed in a system of the cube is strongly normalizing, although this property is not common to all pure type systems. No system in the cube is Turing complete. Subtyping Subtyping however is not represented in the cube, even though systems like , known as higher-order bounded quantification, which combines subtyping and polymorphism are of practical interest, and can be further generalized to bounded type operators. Further extensions to allow the definition of purely