Parametric polymorphism for XML processing languages

XML (eXtensible Markup Language) is a current standard format for exchanging semi-structured data, which has been applied to web services, database, research on formal methods, and so on. For a better processing of XML, recently there emerge many statically typed functional languages, such as XDuce, CDuce, XJ, XTatic, XACT, XHaskell, OCamIDuce and so on. But most of these languages lack parametric polymorphism or present it in a limited form. While parametric polymorphism is needed by XML processing, and it has repeatedly been requested to and discussed in various working groups of standards (e.g., RELAX NG and XQuery). We study in this thesis the techniques to extend parametric polymorphism into XML processing languages. Our solution consists of two parts : a definition of a polymorphic semantic subtyping relation and a definition of a polymorphic calculus. In the first part, we define and study a polymorphic semantic subtyping relation for a type system with recursive, product and arrow types and set-theoretic type connectives (i.e., union, intersection and negation). We introduce the notion of "convexity" on which our solution is built up and prove there exists at least one model that satisfies convexity. We also propose a sound, complete and decidable subtyping algorithm. The second part is devoted to the theoretical definition of a polymorphic calculus, which takes advance of the subtyping relation. The novelty of the polymorphic calculus is to decorate lambda-abstractions with sets of type-substitutions and to lazily propagate type-substitutions at the moment of the reduction. The second part also explores a semi-decidable local inference algorithm to infer the set of type substitutions as well as the compilation of the polymorphic calculus into a variety of CDuce.XML (eXtensible Markup Language) est un format standard pour l'échange de données semi-structurées, qui est utilisé dans les services web, les bases de données, et comme format de sérialisation pour échanger des données entre applications. Afin d'avoir un meilleur traitement de données XML, plusieurs langages statiquement typés pour XML ont été récemment définis, tels XDuce, CDuce, XJ, XTatic, XACT, XHaskell, OCamIDuce. Ces langages peuvent vérifier si un programme n'engendra d'erreurs de types à l'exécution. Mais la plupart de ces langages n'incluent pas le polymorphisme paramétrique ou l'incluent sous une forme très limitée. Cependant, le traitement de données XML nécessite du polymorphisme paramétrique, c'est pourquoi il a été demandé et discuté à plusieurs reprises dans divers groupes de travail de standardisation (par exemple, RELAX-NG et XQuery). Nous étudions dans cette thèse les techniques pour étendre par le polymorphisme paramétrique les langages de traitement XML. Notre solution se déroule sur deux étapes : (i) nous définissons et étudions une relation de sous-typage polymorphe sémantique pour un système de type avec types récursifs, types des produits, types des flèches, et types des ensemblistes (c'est-à-dire, l'union, l'intersection et la négation) ; et (ii) nous concevons et étudions un langage fonctionnel d'ordre supérieur qui tire pleinement parti des nouvelles fonctionnalités du système de type. La solution que nous proposons dans cette thèse est générale. Ainsi elle a des domaines d'application autres que les langages pour le traitement de données XML.PARIS7-Bibliothèque centrale (751132105) / SudocSudocFranceF