Lambda cube (Barendregt)

Layer 0 — Mathematicsin the Type Theory subtree

Barendregt 1991: 8 typed lambda-calculi differing in 3 dependency-axes (terms-on-types, types-on-types, types-on-terms); STLC corner / System F / LF / CoC.