XPath Formal Semantics and Beyond: a Coq based approach

Abstract : XPath was introduced as the standard language for addressing parts of XML documents, and has been widely adopted by practioners and theoreticaly studied. We aim at building a logical framework for formal study and analysis of XPath and have to face the combinatorial complexity of formal proofs caused by XPath expressive power. We chose the Coq proof assistant and its powerful inductive constructions to rigorously investigate XPath peculiarities. We focus in this paper on a basic modeling of XPath syntax and semantics, and make two contributions. First, we propose a new formal semantics, which is an interpretation of paths as first order logic propositions that turned out to greatly simplify our formal proofs. Second, we formally prove that this new interpretation is equivalent to previously known XPath denotational semantics, opening perspectives for more ambitious mathematical characterizations. We illustrate our Coq based model through several examples and we develop a formal proof of a simple yet significant XPath property that compares quite favorably to a former informal proof.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

Contributor : Vincent Quint <>
Submitted on : Friday, October 9, 2009 - 4:19:08 PM
Last modification on : Tuesday, February 12, 2019 - 10:30:05 AM
Long-term archiving on : Wednesday, June 16, 2010 - 12:34:17 AM


Files produced by the author(s)


  • HAL Id : inria-00423372, version 1



Pierre Genevès, Jean-Yves Vion-Dury. XPath Formal Semantics and Beyond: a Coq based approach. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logic: TPHOLs 2004, Aug 2004, Utah, United States. pp.181-198. ⟨inria-00423372⟩



Record views


Files downloads