{"id":62,"date":"2014-10-08T17:13:38","date_gmt":"2014-10-08T15:13:38","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/?p=62"},"modified":"2016-09-27T18:54:30","modified_gmt":"2016-09-27T16:54:30","slug":"welcome","status":"publish","type":"post","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/2014\/10\/08\/welcome\/","title":{"rendered":"Proof systems for data queries"},"content":{"rendered":"<p class=\"prodaq-welcome\">\nWelcome to the home of the prodaq project!  Prodaq is funded by <a href=\"https:\/\/www.agence-nationale-recherche.fr\"><abbr title=\"Agence Nationale de la Recherche\">ANR<\/abbr><\/a> and located at <a href=\"https:\/\/www.lsv.ens-paris-saclay.fr\/\"><abbr title=\"Laboratoire Sp\u00e9cification et V\u00e9rification\">LSV<\/abbr><\/a> in Cachan, France.\n<\/p>\n<h3 class=\"prodaq-welcome\">Context of the Project<\/h3>\n<p class=\"prodaq-welcome\"><a href=\"https:\/\/en.wikipedia.org\/wiki\/Semi-structured_data\">Semi-structured data<\/a>, in particular in the form of <a href=\"https:\/\/www.w3.org\/TR\/xml\/\">XML documents<\/a>, is now the established paradigm for storing and retrieving data over the Internet. <a href=\"https:\/\/www.w3.org\/TR\/xpath\/\">XPath<\/a> is a querying language, which allows to select elements in XML documents. Its use is pervasive in Web-oriented languages like <a href=\"https:\/\/www.w3.org\/TR\/xsl\/\">XSLT<\/a> or <a href=\"https:\/\/www.w3.org\/TR\/xquery\/\">XQuery<\/a>, but also in general-purpose languages like Java or C#. It combines the ability to navigate the XML document\u2014which finds its roots in <a href=\"https:\/\/en.wikipedia.org\/wiki\/Modal_logic\">modal logic<\/a>\u2014with 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.<\/p>\n<p class=\"prodaq-welcome\">The presence of data tests makes the formal verification of XPath queries impossible in general (the problem is <a href=\"https:\/\/en.wikipedia.org\/wiki\/Undecidable_problem\">undecidable<\/a>). The research on restrictions and variants of XPath must therefore seek new standards, algorithms, and languages, which should strike a balance between practical usability\u2014can typical queries be expressed in the restricted language?\u2014and amenability to formal analysis\u2014can 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.<\/p>\n<p class=\"prodaq-welcome\">The originality of the approach in the prodaq project is the use of <a href=\"https:\/\/en.wikipedia.org\/wiki\/Proof_calculus\">proof systems<\/a> to this end. We hope to draw inspiration notably from proof-theoretic approaches to modal logics and <A href=\"https:\/\/en.wikipedia.org\/wiki\/Automata_theory\">automata<\/a>.  The project also investigates the connection between data and <a href=\"https:\/\/en.wikipedia.org\/wiki\/Substructural_logic\">substructural connectives<\/a>, and the use of <a href=\"https:\/\/en.wikipedia.org\/wiki\/Counter_machine\">counter systems<\/a> as a means to obtain <a href=\"https:\/\/en.wikipedia.org\/wiki\/Algorithm\">algorithms<\/a> and <a href=\"https:\/\/en.wikipedia.org\/wiki\/Computational_complexity_theory\">complexity<\/a> results on both data and substructural logics.<\/p>\n<p class=\"prodaq-welcome\">To learn more about the project:<\/p>\n<ul id=\"prodaq-menu\">\n<li><a href=\"welcome\">Presentation<\/a><\/li>\n<li><a href=\"participants\">Participants<\/a><\/li>\n<li><a href=\"publications\">Publications<\/a><\/li>\n<li><a href=\"releases\">Releases<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>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 [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":true,"template":"","format":"aside","meta":{"footnotes":""},"categories":[13],"tags":[10,2],"class_list":["post-62","post","type-post","status-publish","format-aside","hentry","category-explanations","tag-proof","tag-xpath","post_format-post-format-aside"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/posts\/62","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/comments?post=62"}],"version-history":[{"count":20,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/posts\/62\/revisions"}],"predecessor-version":[{"id":164,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/posts\/62\/revisions\/164"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/media?parent=62"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/categories?post=62"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/prodaq\/wp-json\/wp\/v2\/tags?post=62"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}