Typage d'un système de modules paramétriques avec partage : une application de l'unification dans les théories équationnelles / Maria Virginia Aponte ; sous la direction de Guy Cousineau

Bibliogr. p. 164-166

Thèse de doctorat informatique fondamentale 1992 Paris 7

ModL est un langage pour la décomposition modulaire de programmes, indépendant de tout langage de base et explicitement typé. Il possède des modules paramétriques, une notion d'inclusion de sous-modules et la possibilité de contraindre des sous-modules à être partagés. ModL est inspiré du langage de modules de SML, qui est un langage fonctionnel de la famille ML. Nous donnons une méthode conceptuellement simple, efficace et précise pour typer ModL. Elle est simple car le codage des notions d'inclusion et de partage repose entièrement sur les théories bien connues d'unification et de polymorphisme. Elle est efficace car les vérifications de cohérence deviennent entièrement locales et ne dépendent que de l'unifiabilité des termes, ce qui permet d'écarter plus rapidement des types incorrects. Elle est enfin très précise car elle permet d'extraire à partir des règles un algorithme de typage complet