Master project description
TITLE: XML, Types, mu-calculus and solvers
In recent years, temporal logic has been introduced successfully in the context of XML programming and databases as a foundation for representing and reasoning about Tree Types [1, 2, 3]. In particular, such logics offer a unifying formalism for core programming constructs such as XML schemas (XML Schema, Relax NG, DTDs) and query languages such as XPath and XQuery. They have also nice algorithmic properties that allow obtaining efficient evaluation and reasoning solvers (see [8]). The purpose of this work is to propose a general theory to enhance the compositional, reuse and synthesis capabilities of XML types [1,4]. More precisely, this proposition covers two different, while related, interships proposals, namely:
  1. Polymorphism, arrow types and Mu-calcul:
    A first research track concerns adding polymorphism to CDuce's semantic subtyping. Adding polymorphism to CDuce's type system is algorithmically very complex insofar as several weird (presence of intersections, negations, unions) constraints are to be dealt with. A first step will aim at adding, either natively or by an encoding, an arrow constructor to mu-calculus expressions and use the solveur to decide subtyping. In a second phase, it will be necessary to introduce type variables to mu-calculus (introducing quantifiers in formulae). A second research track consists in studying polymorphism for the types that are inferred by the solver for transformations. Indeed, the solver (see [8]) can infer a type for both the source and the result of an XPath expression. An idea could be to annotate the input type and track dependencies between input and output variables so as to accurately detect copies between input and output types.
  2. Relevant nodes, XPath evalution and solver bounds :
    A first goal will be to understand how backward modalities are managed by the solver and then apply similar techniques to add "up-move" transitions in the automata defined in [8]. In a second phase we shall concentrate our work on the sound definition of relevant nodes for a given schema. It is claimed that such a definition is closely related to the one of the solver's maximal tree: the smallest tree in terms of height which generates all counter examples.
Required background
  • Strong background in functional programming.
  • Type theory, Autoamata and tree automata
  • Reasonable acquaintance with XPath/XQuery
  • [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.