Dependent Types

- Natural & Formal Sciences -
Mathematics & Logic Dictionary
A type-theoretic feature and family of systems in which types may depend on values (terms), enabling types to express precise specifications, relate data and proofs, and internalize propositions as types.