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.

Giuseppe Castagna : PPS Laboratory, Université Paris 7.
Véronique Benzaken : Proval project team INRIA - Saclay and LRI Laboratory, Université Paris Sud.
Nabil Layaïda : WAM project team, Inria Rhone Alpes