Showing content from http://homepages.inf.ed.ac.uk/jcheney/projects/XQuery below:
Mechanizing the metatheory of mini-XQuery
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
RetroSearch is an open source project built by @garambo
| Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.3