dependently typed programming language
C39238
concept
A dependently typed programming language is one in which types can depend on values, enabling the expression and static verification of rich logical properties directly in the type system.