Mechanizing the Metatheory of mini-XQuery

James Cheney, Christian Urban

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationCertified Programs and Proofs
Subtitle of host publicationFirst International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings
EditorsJean-Pierre Jouannaud, Zhong Shao
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-642-25379-9
ISBN (Print)978-3-642-25378-2
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'Mechanizing the Metatheory of mini-XQuery'. Together they form a unique fingerprint.

Cite this