ML dépendant - Dependent ML

Dependent ML est un langage de programmation fonctionnel expérimental proposé par Hongwei Xi ( Xi 2007 ) et Frank Pfenning . Le ML dépendant étend le ML par une notion restreinte de types dépendants : les types peuvent dépendre d'indices statiques de type Nat ( nombres naturels ). Le ML dépendant utilise un prouveur de théorème de contrainte pour décider d'une théorie équationnelle forte sur les expressions d'indice.

Les types de DML ne dépendent pas des valeurs d'exécution - il existe toujours une distinction de phase entre la compilation et l'exécution du programme. En restreignant la généralité des types entièrement dépendants, la vérification de type reste décidable , mais l' inférence de type devient indécidable.

Le ML dépendant a été remplacé par ATS et n'est plus en cours de développement actif.

Les références

Lectures complémentaires

  • Xi, Hongwei (mars 2007). "ML dépendant: une approche à la programmation pratique avec des types dépendants" . Journal de programmation fonctionnelle . 17 (2): 215-286. doi : 10.1017 / S0956796806006216 . S2CID   45996427 .
  • David Aspinall et Martin Hofmann (2005). "Types dépendants". Dans Pierce, Benjamin C. (ed.) Advanced Topics in Types and Programming Languages . MIT Press.

Liens externes


Icône de talon

Cet article relatif au langage de programmation est un bout . Vous pouvez aider Wikipédia en le développant .