Lambda cube

Summary

The lambda cube is a family of eight typed lambda calculi, arranged as the vertices of a cube. It starts from the simply typed lambda calculus and adds three kinds of dependency independently. They are terms depending on types, types depending on types, and types depending on terms. Adding all three gives the calculus of constructions; adding only the first gives System F. Henk Barendregt introduced it in 1991 to compare these systems inside one framework of type theory.