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 (natural numbers). Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions. Dependent ML has been superseded by ATS and is no longer under active development.

Property Value
dbo:abstract
  • 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 (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 phase distinction between compilation and execution of the program. By restricting the generality of full dependent types type checking remains decidable, but type inference becomes undecidable. Dependent ML has been superseded by ATS and is no longer under active development. (en)
dbo:wikiPageEditLink
dbo:wikiPageExternalLink
dbo:wikiPageExtracted
  • 2019-06-09 18:16:12Z (xsd:date)
dbo:wikiPageHistoryLink
dbo:wikiPageID
  • 1951390 (xsd:integer)
dbo:wikiPageLength
  • 1853 (xsd:integer)
dbo:wikiPageModified
  • 2018-08-29 23:31:30Z (xsd:date)
dbo:wikiPageOutDegree
  • 20 (xsd:integer)
dbo:wikiPageRevisionID
  • 857161663 (xsd:integer)
dbo:wikiPageRevisionLink
dbp:wikiPageUsesTemplate
dct:subject
rdf:type
rdfs:comment
  • 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 (natural numbers). Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions. Dependent ML has been superseded by ATS and is no longer under active development. (en)
rdfs:label
  • Dependent ML (en)
owl:sameAs
foaf:isPrimaryTopicOf
is dbo:influencedBy of
is dbo:wikiPageRedirects of
is foaf:primaryTopic of