Algèbres touffues: application au typage polymorphe des objets enregistrements dans les langages fonctionnels / Didier Rémy

Auteur: Rémy, Didier (1963-) - AuteurAuteur secondaire : Huet, Gérard (1947-) - Directeur de thèseCollectivité secondaire: Université Paris Diderot - Paris 7 - Etablissement de soutenanceType de document: ThèseLangue: françaisPays: FranceÉditeur: [S.l.] : [s.n.], 1990Description: 1 vol. (171 p.) ; 30 cm ISBN: 2726106153 ; br. Résumé: Le langage ml est un langage fonctionnel type polymorphe avec synthese de types. Nous proposons une solution simple pour etendre ml avec des objets enregistrements avec heritage tout en conservant la synthese des types. Simplicite, car les regles de typage de ml ne sont pas modifiees et l'heritage provient uniquement du polymorphisme des operations sur les objets enregistrements. Les objets enregistrements sont des fonctions partielles de domaines finis d'un ensemble denombrable d'etiquettes vers l'ensemble des valeurs. Nous leur associons des types enregistrements qui sont des fonctions partielles de l'ensemble des etiquettes vers l'ensemble des types, que nous rendons totales en definissant des types par defaut pour les etiquettes absentes. Les types enregistrements sont representables de maniere finie dans une algebre de termes munie d'une famille d'equations de distributivite et de commutativite gauche tres severement controlees par des sortes. Nous montrons que cette theorie equationnelle est syntaxique, et nous en deduisons facilement que l'unification y est decidable et unitaire. Puis nous montrons que l'algebre des types de ml peut etre etendue avec une theorie equationnelle reguliere pour laquelle le probleme d'unification est decidable et unitaire. Le langage obtenu est parametre par le jeu de primitives fournies avec leurs types qui realisent les operations elementaires sur les enregistrements. Cette methode devrait s'etendre a des types recursifs et s'appliquer a d'autres langages que ml, notamment a des langages avec l'inclusion de types.Bibliographie: Bibliogr. p. 165-168.Thèse: Thèse de doctorat en informatique, soutenue en 1990, organisme : université Paris VII Sujets MSC: 68N15 Computer science -- Software -- Programming languages
68Q70 Computer science -- Theory of computing -- Algebraic theory of languages and automata
97A70 Mathematics education - General, mathematics and education -- Theses and postdoctoral theses
Location Call Number Status Date Due
Salle S 10452-01 / Thèses REM (Browse Shelf) Available

Bibliogr. p. 165-168

Thèse de doctorat informatique 1990 université Paris VII

Le langage ml est un langage fonctionnel type polymorphe avec synthese de types. Nous proposons une solution simple pour etendre ml avec des objets enregistrements avec heritage tout en conservant la synthese des types. Simplicite, car les regles de typage de ml ne sont pas modifiees et l'heritage provient uniquement du polymorphisme des operations sur les objets enregistrements. Les objets enregistrements sont des fonctions partielles de domaines finis d'un ensemble denombrable d'etiquettes vers l'ensemble des valeurs. Nous leur associons des types enregistrements qui sont des fonctions partielles de l'ensemble des etiquettes vers l'ensemble des types, que nous rendons totales en definissant des types par defaut pour les etiquettes absentes. Les types enregistrements sont representables de maniere finie dans une algebre de termes munie d'une famille d'equations de distributivite et de commutativite gauche tres severement controlees par des sortes. Nous montrons que cette theorie equationnelle est syntaxique, et nous en deduisons facilement que l'unification y est decidable et unitaire. Puis nous montrons que l'algebre des types de ml peut etre etendue avec une theorie equationnelle reguliere pour laquelle le probleme d'unification est decidable et unitaire. Le langage obtenu est parametre par le jeu de primitives fournies avec leurs types qui realisent les operations elementaires sur les enregistrements. Cette methode devrait s'etendre a des types recursifs et s'appliquer a d'autres langages que ml, notamment a des langages avec l'inclusion de types

There are no comments for this item.

Log in to your account to post a comment.
Languages: English | Français | |