Intégration des approches langage, logique et orientée données pour un traitement XML certifié, dirigé par les types. – TYPEX

Les trois partenaires de cette proposition travaillent au développement de méthodes formelles
permettant de définir des transformations de documents XML de manière aisée, d'y appliquer des
analyses statiques et de les implanter efficacement. Pour atteindre ce but, chaque partenaire
utilise une approche différente (chacun des partenaire est un expert reconnu de son domaine).
L'équipe WAM suit une approche basée sur un solveur pour la logique du mu-calcul, la composante PPS
utilise des techniques issues des langages de programmation, et l'équipe du LRI celles des langages
orientés données. Ces approches permettent d'obtenir différents résultats et de manière
intéressante, mais guère surprenante, les points forts des uns sont souvent les faiblesses (ou les
"travaux futurs") des autres. L'objectif de ce projet est de provoquer un changement radical du
paradigme de manipulation de données XML.

Pour atteindre ce but, nous allons mettre en commun les expériences et le savoir-faire de chaque
groupe afin d'améliorer dans un premier temps, par enrichissement mutuel, la recherche dans chacun
des trois domaines et ensuite de les intégrer dans un cadre unique. En premier lieu, nous comptons
utiliser les techniques des langages fonctionnels pour ajouter au mu-calcul du solveur des variables
polymorphes et s'en servir pour analyser statiquement des transformations effectuées par les moteurs
de requêtes XML. Les techniques développées pour le solveur seront elles utilisées pour ajouter le
traitement des axes arrières aux automates d'arbres utilisés pour l'évaluation efficace de requêtes
XML natives. Nous modifierons le solveur pour l'utiliser dans le cadre de la résolution des
contraintes engendrées lors du typage de l'application de fonctions polymorphes. Les développements
formels sur la théorie des automates seront réutilisés pour l'implantation de requêtes XML, pour
définir des itérateurs et pour étudier la parallélisation de langages fonctionnels manipulant les
documents XML. Nous enrichirons le solveur (ou sa méta-théorie) en utilisant les techniques de
typage des langages orientés XML, afin de lui ajouter l'ordre supérieur et les transformations
polymorphes. Nous proposons aussi de transposer les techniques d'analyse statique des langages
généralistes aux langages spécifiques pour XML. En particulier, nous utiliserons l'assistant de
preuve Coq pour développer une spécification formelle d'XPath, des automates d'arbres et du
mu-calcul, pour vérifier les implantations du solveur et du moteur de requête vis-à-vis de ces
spécifications et garantir formellement leurs performances.

L'objectif final du projet est des plus ambitieux. Notre but est de proposer une nouvelle génération
de langages de programmation pour XML, résultant de la réunion et de l'intégration des trois
approches dans un cadre unique. Des langages dont les fondements seront inspirés par les derniers
résultats de la recherche en langages de programmation, dotés de systèmes de type précis et
polymorphes combinant le typage classique avec des approches basées sur les solveurs logiques; munis
d'implantations efficaces issues des derniers développements dans le domaine des automates d'arbres
et prouvées formellement par les dernières techniques de raisonnement formel; des langages dont
les optimisations seront guidées par les systèmes de types et les formalisations logiques et dont
l'efficacité sera garantie formellement; des langages offrant la possibilité de spécifier et de
vérifier statiquement des invariants, des règles de comportement et l'intégrité des données. Des
langages avec un impact direct et immédiat sur les processus de standardisation.