Parametric Polymorphism and Semantic Subtyping: the Logical Connection

Nils Gesbert 1, * Pierre Genevès 1 Nabil Layaïda 1
* Corresponding author
1 WAM - Web, adaptation and multimedia
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.
Document type :
Conference papers
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

Cited literature [16 references]  Display  Hide  Download

https://hal.inria.fr/inria-00585686
Contributor : Nils Gesbert <>
Submitted on : Tuesday, September 6, 2011 - 11:26:13 AM
Last modification on : Thursday, October 11, 2018 - 8:48:03 AM
Document(s) archivé(s) le : Thursday, March 30, 2017 - 2:29:00 PM

File

icfp99-gesbert.pdf
Files produced by the author(s)

Identifiers

Collections

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〉

Share

Metrics

Record views

573

Files downloads

332