We present a Nominal Isabelle formalization of an expressive core fragment of XQuery, a W3C standard functional language for querying XML documents. Our formalization focuses on results presented in the literature concerning XQuery's operational semantics, typechecking, and optimizations. Our core language, called mini-XQuery, omits many complications of XQuery such as ancestor and sibling axes, recursive types and functions, node identity, and unordered processing modes, but does handle distinctive features of XQuery including monadic comprehensions, downward XPath steps and regular expression types. To our knowledge no language with similar features has been mechanically formalized previously. Our formalization is a first step towards a complete formalization of full XQuery. © 2011 Springer-Verlag.
CITATION STYLE
Cheney, J., & Urban, C. (2011). Mechanizing the metatheory of mini-XQuery. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7086 LNCS, pp. 280–295). https://doi.org/10.1007/978-3-642-25379-9_21
Mendeley helps you to discover research relevant for your work.