Dependent

Type system where types depend on terms, allowing for more expressive type constraints.