Propositions de stage M2
TITRE: Autour d'XML, Types, mu-calcul et solveurs
La logique temporelle s'avère être un outil formel particulièrement adapté au traitement et à la représentation des données au format XML. En particulier, cette logique constitue un formalisme unificateur pour la représentation des types XML (XML Schema, Relax NG, DTDs) ainsi que des langages de navigation ou d'interrogation tels XPath et XQuery. En outre ces logiques possèdent de bonnes propriétés algorithmiques qui permettent la définition et l'implantation de solveurs efficaces (cf., [8]). L'objectif de ce stage est de se fonder sur ce cadre théorique général pour l'étude de l'un de ces deux problèmes:
  1. Polymorphisme, types flèches et Mu-calcul:
    L'ajout du polymorphisme au sous-typage dans CDuce est difficile algorithmiquement (système de contraintes étranges avec intersections/union/négation....). Une piste consistera à ajouter (soit de façon native soit par encodage) la flèche aux expressions du mu-calcul et d'utiliser le solveur pour décider le sous-typage. Il faudra ensuite introduire les variables de types au mu-calcul (par exemple en introduisant des quantificateurs dans les formules). Une seconde piste consiste à étudier le polymorphisme pour les types des transformations inférés par le solveur. En effet, notre solveur (voir [8]) permet d'inférer un type pour l'argument et le résultat d'un chemin XPath. Une idée est d'étiqueter le type d'entrée et de tracker les dépendances entre variables du type d'entrée et du type de sortie (pour détecter finement les copies entre types d'entrée et de sortie).
  2. Noeuds pertinants évaluations XPath et borne pour le solveur :
    Un premier objectif sera de comprendre comment les modalités arrière sont gérées par le solveur et d'appliquer les mêmes techniques pour ajouter les «up-move» dans les automates définis dans [8]. Dans un second temps, il faudra travailler sur une notion de noeuds pertinents pour une requête et un schéma. Il semble que cette notion soit la même que celle d'arbre maximal (i.e. le plus petit arbre en termes de hauteur qui génère tous les arbres contre-exemple) pour le solveur.
Pré-requis
  • Bonne connaissance de la programmation fonctionnelle
  • Connaissance théorie des types, automates et automates d'arbre
  • Connaissance raisonnable des langages XPath/XQuery
Bibliographie
  • [1] Efficient Static Analysis of XML Paths and Types, Pierre Geneves, Nabil Layaida and Alan Schmitt, PLDI'07.
  • [2] An Automata-Theoretic Approach to Regular XPath, D. Calvanese, G. De Giacomo, M. Lenzerini and M. Vardi, DBPL'09.
  • [3] Reasoning about XML with temporal logics and automata. Leonid Libkin and Cristina Sirangelo. Journal of Applied Logic, 8 (2) (2010), 210-232.
  • [4] Véronique Benzaken, Giuseppe Castagna, Dario Colazzo, and Kim Nguyen. Type-Based XML Projection. VLDB'06.
  • [5] Query Identifying Incompatibilities With Evolving XML Schemas, Pierre Geneves, Nabil Layaida and Vincent Quint, ICFP'09.
  • [6] Semantic Subtyping: dealing set-theoretically with function, union, intersection and negation types A. Frisch, G. Castagna and V. Benzaken , In Journal of the ACM (JACM) Volume 55 , Issue 4 (September 2008).
  • [7] CDuce: an XML-centric general purpose programming language, V. Benzaken , G. Castagna and A. Frisch, in Proc of the international conference on functional programming (ICFP'03), Upsala, Sweden, 25-29 august 2003
  • [8] Reasoning solvers.