Mechanizing the metatheory of mini-XQuery
James Cheney and Christian Urban
This is a formalization in
Nominal Isabelle of
the basic metatheory of mini-XQuery. Mini-XQuery is a core calculus
for XQuery, a W3C standard
XML query language. Mini-XQuery is not full XQuery but includes many
distinctive features, including descendant and child steps, filters,
and comprehensions, and it is similar to other core languages for
XQuery that have been introduced and used in the literature, including
Core XQuery and muXQ; thus, results about these other languages can be
proved in mini-XQuery without much adjustment. Ultimately, we plan to
develop a full-scale formalization of XQuery's Formal Semantics,
including features that are not treated fully formally there, such as
node identity; we would also like to define and formalize the
semantics of XQuery
Updates. We hope that this kind of work can contribute to and
complement W3C standardization activities for future versions of
XQuery.
A paper
(CPP 2011)
accompanying the formalization provides further details of the
development.
Theory files
- XQuery.thy - the main theory defining
the syntax, semantics and type system of mini-XQuery
- Equivalence.thy - some results
concerning operational equivalence of mini-XQuery expressions,
including congruences and simplification rules for comprehensions.
- Subtyping.thy - some results
concerning subtyping of regular expression types in mini-XQuery
Last modified: Tue Aug 30 09:39:30 PDT 2011