Proof systems for data queries
Welcome to the home of the prodaq project! Prodaq is funded by ANR and located at LSV in Cachan, France.
Context of the Project
Semi-structured data, in particular in the form of XML documents, is now the established paradigm for storing and retrieving data over the Internet. XPath is a querying language, which allows to select elements in XML documents. Its use is pervasive in Web-oriented languages like XSLT or XQuery, but also in general-purpose languages like Java or C#. It combines the ability to navigate the XML document—which finds its roots in modal logic—with that of comparing data values found in several, distantly related elements. The static analysis of data queries, expressed in XPath or in related data logics, aims to optimize and verify queries.
The presence of data tests makes the formal verification of XPath queries impossible in general (the problem is undecidable). The research on restrictions and variants of XPath must therefore seek new standards, algorithms, and languages, which should strike a balance between practical usability—can typical queries be expressed in the restricted language?—and amenability to formal analysis—can we check queries written in the language? Our main objective is to provide rigorous foundations for automatic analysis tools that verify queries in data-centric programs.
The originality of the approach in the prodaq project is the use of proof systems to this end. We hope to draw inspiration notably from proof-theoretic approaches to modal logics and automata. The project also investigates the connection between data and substructural connectives, and the use of counter systems as a means to obtain algorithms and complexity results on both data and substructural logics.
To learn more about the project: