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

Contributeur : Tyrex Equipe <>
Soumis le : lundi 17 août 2015 - 13:21:41
Dernière modification le : jeudi 11 octobre 2018 - 08:48:04
Document(s) archivé(s) le : mercredi 26 avril 2017 - 09:53:36


Fichiers produits par l'(les) auteur(s)




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〉



Consultations de la notice


Téléchargements de fichiers