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. 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. 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. Some computer scientists do not consider DML's types to be dependent as there is still a phase distinction between compilation and execution of the program. Dependent ML has been superseded by ATS and is no longer under active development. (en)
  • Dependent ML (зависимый метаязык) — экспериментальный функциональный язык программирования, разработанный Фрэнком Пфеннингом и Хонвеем Хи. Dependent ML расширяет язык программирования ML путём ограничения представления зависимых типов: типы могут зависеть от статических указателей типа Nat. Dependent ML основывается на ограниченном доказательстве теорем для вывода теории строго равенства через индексные выражения. Dependent ML был замещен языком ATS и по этой причине в фазе активной разработки больше не находится. (ru)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1951390 (xsd:integer)
dbo:wikiPageRevisionID
  • 704762304 (xsd:integer)
dct:subject
http://purl.org/linguistics/gold/hypernym
rdf:type
rdfs:comment
  • Dependent ML (зависимый метаязык) — экспериментальный функциональный язык программирования, разработанный Фрэнком Пфеннингом и Хонвеем Хи. Dependent ML расширяет язык программирования ML путём ограничения представления зависимых типов: типы могут зависеть от статических указателей типа Nat. Dependent ML основывается на ограниченном доказательстве теорем для вывода теории строго равенства через индексные выражения. Dependent ML был замещен языком ATS и по этой причине в фазе активной разработки больше не находится. (ru)
  • 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. Dependent ML has been superseded by ATS and is no longer under active development. (en)
rdfs:label
  • Dependent ML (en)
  • Dependent ML (ru)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:influencedBy of
is dbo:wikiPageRedirects of
is dbp:dialects of
is foaf:primaryTopic of