Tags: Programming Language.

Dependent ML is an experimental functional programming language proposed by Hongwei Xi and Frank Pfenning. 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.By restricting the generality of full dependent types type checking remains decidable. Type inference remains undecidable.

Loading...

This page contains content from the copyrighted Wikipedia article "Dependent ML"; that content is used under the GNU Free Documentation License (GFDL). You may redistribute it, verbatim or modified, providing that you comply with the terms of the GFDL.