Typeful certified XML: : integrating language, logic, and data-oriented best practices. – TYPEX

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.