All the three partners of this proposal work at developing formal techniques to smoothly define, statically analyze, efficiently implement and optimize, transformations of documents in XML format. To reach its objectives each partner uses a different approach (in which they have a world renowned expertise): a logical approach based on solvers for WAM, a programming language (PL) approach for PPS, and a data-oriented approach for LRI. Each approach achieves different goals and interestingly, though not surprisingly, the strengths of the one are often the weaknesses (or the “future work” issues) of the other. The objective of this project is to produce a paradigm shift for the manipulation of XML data. In order to achieve this goal we will mutualize experiences and know-how of each group and use them first to improve, by cross-fertilization, the research in each specific domain, and then to integrate them into a unique framework. Accordingly, we plan to use functional languages techniques to enrich the µ-calculus of our solver with polymorphic variables and to statically analyze (in order to efficiently materialize) transformations in XML engines. We will reengineer the techniques we developed for the solver to handle backward axes so as to enrich with upward moves the automata used to efficiently query native XML engines. We will modify the solver to fit the resolution of constraint systems generated in the type inference of the application of polymorphic functions. We will use the automata theories developed for querying XML systems to define iterators and study the parallelization of functional languages to manipulate XML. We will adapt the techniques used for typing XML programming languages to enrich the solver (or its meta-theory) with higher-order polymorphic transformations. We will transpose the PL techniques developed for static analysis of programs. to standard processing languages for XML data. We will use the Coq proof assistant to develop formal specifications for XPath, tree automata, and µ-calculus (the core tools of our project), verify the implementations of the solver and of the query engine against these specifications, and formally guarantee their efficiency. The highly ambitious and final goal of this project is to produce a new generation of XML programming languages stemming from the synergy of integrating the three approaches into a unique framework. Languages whose constructions are inspired by the latest results in the PL research; with precise and polymorphic type systems that merge PL typing techniques with logical-solver-based type inference; with efficient implementations issued by latest researches on tree automata and formally certified by latest theorem prover technologies; with optimizations directly issued from their types systems and the logical formalizations and whose efficiency will be formally guaranteed; with the capacity to specify and formally verify invariants, business rules, and data integrity. Languages with a direct and immediate impact on standardization processes.