Parametric Polymorphism and Semantic Subtyping: the Logical Connection

Nils Gesbert 1, * Pierre Genevès 1 Nabil Layaïda 1
* Auteur correspondant
1 WAM - Web, adaptation and multimedia
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Résumé : Nous considérons une algèbre de types comprenant des types récursifs, produits, fonctions, intersection, union et négation, ainsi que des variables de types soumises à une quantification universelle implicite. Nous considérons la relation de sous-typage définie récemment par Castagna et Xu sur cette algèbre de types et montrons que cette relation est décidable en EXPTIME, résolvant une question ouverte. La nouveauté, l'originalité et la force de notre solution résident dans l'introduction d'une modélisation logique du sous-typage sémantique. Nous représentons ce sous-typage dans une logique d'arbres et utilisons un algorithme de vérification de satisfaisabilité pour décider la relation. Nous présentons une implémentation complète du système et le résultat de plusieurs tests pratiques.
Type de document :
Communication dans un congrès
International conference on functional programming, Sep 2011, Tokyo, Japan. pp.107-116, 2011, Proceeding of the 16th ACM SIGPLAN international conference on Functional programming. <10.1145/2034773.2034789>
Liste complète des métadonnées

https://hal.inria.fr/inria-00585686
Contributeur : Nils Gesbert <>
Soumis le : mardi 6 septembre 2011 - 11:26:13
Dernière modification le : mardi 18 octobre 2011 - 17:13:15

Fichier

icfp99-gesbert.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIG | UGA

Citation

Nils Gesbert, Pierre Genevès, Nabil Layaïda. Parametric Polymorphism and Semantic Subtyping: the Logical Connection. International conference on functional programming, Sep 2011, Tokyo, Japan. pp.107-116, 2011, Proceeding of the 16th ACM SIGPLAN international conference on Functional programming. <10.1145/2034773.2034789>. <inria-00585686v2>

Partager

Métriques

Consultations de
la notice

297

Téléchargements du document

149