出典:Wikipedia
出典:『Wikipedia』 (2011/06/01 12:31 UTC 版)
Dependent ML is an experimental functional programming language proposed by Frank Pfenning and Hongwei Xi. 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.