Dependent ML (DML) is an experimental, multi-paradigm, general-purpose, high-level, functional programming language proposed by Hongwei Xi and Frank Pfenning. It is a dialect of the programming language ML. Dependent ML extends ML by a restricted notion of dependent types: types may be dependent on static indices of type Nat. Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions.