Dependent ML
 | This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages)
|
Dependent ML is an experimental
dependent types: types may be dependent on static indices of type Nat (natural numbers
). Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions.
DML's types are not dependent on runtime values - there is still a
type checking remains decidable, but type inference
becomes undecidable.
Dependent ML has been superseded by ATS and is no longer under active development.
References
- ^ Aspinall & Hofmann 2005. p. 75.
Further reading
- Xi, Hongwei (March 2007). "Dependent ML: An Approach to Practical Programming with Dependent Types". S2CID 45996427.
- David Aspinall and Martin Hofmann (2005). "Dependent Types". In Pierce, Benjamin C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press.
External links
- Official website, Hongwei Xi, ATS designer, maintainer
- The home page of DML Archived 2009-12-13 at the Wayback Machine
| |||||||||
| Programming tools | |||||||||
| Theorem provers, proof assistants | |||||||||
| Designers |
|---|
Book 
Category:Family:ML Category:Family:OCaml Category:Software:OCaml
 | This programming-language-related article is a stub. You can help Wikipedia by expanding it. |