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

Last modified: Tue Aug 30 09:39:30 PDT 2011