Parametric Polymorphism and Semantic Subtyping: the Logical Connection

International audienceWe 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.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