A Logical Approach To Deciding Semantic Subtyping

Nils Gesbert 1 Pierre Genevès 1 Nabil Layaïda 1
1 TYREX - Types and Reasoning for the Web
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : We consider a type algebra equipped with recursive, product, function, intersection, union, and complement types together with type variables and implicit universal quantification over them. We consider the subtyping relation recently defined by Castagna and Xu over such type expressions and show how this relation can be decided in EXPTIME, answering an open question. The novelty, originality and strength of our solution reside in introducing a logical modeling for the semantic subtyping framework. We model semantic subtyping in a tree logic and use a satisfiability-testing algorithm in order to decide subtyping. We report on practical experiments made with a full implementation of the system. This provides a powerful polymorphic type system aiming at maintaining full static type-safety of functional programs that manipulate trees, even with higher-order functions, which is particularly useful in the context of XML.
Type de document :
Article dans une revue
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2015, 38 (1), pp.31. 〈http://toplas.acm.org/〉. 〈10.1145/2812805〉
Domaine :
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00848023
Contributeur : Tyrex Equipe <>
Soumis le : lundi 17 août 2015 - 13:21:41
Dernière modification le : mercredi 14 décembre 2016 - 01:08:46
Document(s) archivé(s) le : mercredi 26 avril 2017 - 09:53:36

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Nils Gesbert, Pierre Genevès, Nabil Layaïda. A Logical Approach To Deciding Semantic Subtyping. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2015, 38 (1), pp.31. 〈http://toplas.acm.org/〉. 〈10.1145/2812805〉. 〈hal-00848023v2〉

Partager

Métriques

Consultations de
la notice

225

Téléchargements du document

117