A Logical Approach To Deciding Semantic Subtyping - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue ACM Transactions on Programming Languages and Systems (TOPLAS) Année : 2015

A Logical Approach To Deciding Semantic Subtyping

Nils Gesbert
  • Fonction : Auteur
  • PersonId : 958488
Pierre Genevès
Nabil Layaïda

Résumé

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.

Domaines

Web
Fichier principal
Vignette du fichier
article.pdf (490.14 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00848023 , version 1 (25-07-2013)
hal-00848023 , version 2 (17-08-2015)

Identifiants

Citer

Nils Gesbert, Pierre Genevès, Nabil Layaïda. A Logical Approach To Deciding Semantic Subtyping. ACM Transactions on Programming Languages and Systems (TOPLAS), 2015, 38 (1), pp.31. ⟨10.1145/2812805⟩. ⟨hal-00848023v2⟩
262 Consultations
456 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More