Advertisement

Mechanizing the Metatheory of mini-XQuery

  • James Cheney
  • Christian Urban
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)

Abstract

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.

Keywords

Operational Semantic Typing Context Type Soundness Typing Judgment Core Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Babu, C.S., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL, pp. 3–15 (2008)Google Scholar
  3. 3.
    Benedikt, M., Cheney, J.: Semantics, Types and Effects for XML Updates. In: Gardner, P., Geerts, F. (eds.) DBPL 2009. LNCS, vol. 5708, pp. 1–17. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  4. 4.
    Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science 5(2) (2008)Google Scholar
  5. 5.
    Berghofer, S., Urban, C.: Nominal Inversion Principles. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 71–85. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Boag, S., Chamberlin, D., Fernández, M.F., Florescu, D., Robie, J., Siméon, J.: XQuery 1.0: An XML query language. W3C Recommendation (January 2007), http://www.w3.org/TR/xquery
  7. 7.
    Chamberlin, D., Robie, J.: XQuery update facility 1.0. W3C Candidate Recommendation (August 2008), http://www.w3.org/TR/xquery-update-10/
  8. 8.
    Cheney, J.: Regular Expression Subtyping for XML Query and Update Languages. In: Gairing, M. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 32–47. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Cheney, J., Urban, C.: Formalization of mini-XQuery in Nominal Isabelle, http://homepages.inf.ed.ac.uk/jcheney/projects/XQuery
  10. 10.
    Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP, pp. 143–156 (2008)Google Scholar
  11. 11.
    Chlipala, A., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: ICFP, pp. 79–90 (2009)Google Scholar
  12. 12.
    Colazzo, D., Ghelli, G., Manghi, P., Sartiani, C.: Static analysis for path correctness of XML queries. J. Funct. Program. 16(4-5), 621–661 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Colazzo, D., Sartiani, C.: Precision and complexity of XQuery type inference. In: PPDP (to appear, 2011); Preliminary version in ICTCS 2010Google Scholar
  14. 14.
    Fernandez, M., Siméon, J., Wadler, P.: A Semi-Monad for Semi-Structured Data. In: Van den Bussche, J., Vianu, V. (eds.) ICDT 2001. LNCS, vol. 1973, pp. 263–300. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002)CrossRefzbMATHGoogle Scholar
  16. 16.
    Gacek, A.: The Abella Interactive Theorem Prover (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Genevès, P., Vion-Dury, J.-Y.: XPath formal semantics and beyond: A Coq-based approach. In: TPHOLs Emerging Trends, Salt Lake City, Utah, United States, August 2004, pp. 181–198. University Of Utah (2004)Google Scholar
  18. 18.
    Grust, T., Rittinger, J., Teubner, J.: Pathfinder: XQuery off the relational shelf. IEEE Data Eng. Bull. 31(4) (2008)Google Scholar
  19. 19.
    Hosoya, H., Vouillon, J., Pierce, B.C.: Regular expression types for XML. ACM Trans. Program. Lang. Syst. 27(1), 46–90 (2005)CrossRefzbMATHGoogle Scholar
  20. 20.
    Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: POPL, pp. 237–248 (2010)Google Scholar
  21. 21.
    Pfenning, F., Schürmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  22. 22.
    Ré, C., Siméon, J., Fernández, M.F.: A complete and efficient algebraic compiler for XQuery. In: ICDE, p. 14 (2006)Google Scholar
  23. 23.
    Rose, K.: CRSX - combinatory reduction systems with extensions. In: RTA (2011)Google Scholar
  24. 24.
    Siméon, J., Wadler, P.: The essence of XML. In: POPL, New York, NY, USA, pp. 1–13. ACM (2003)Google Scholar
  25. 25.
    Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reasoning 40(4), 327–356 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Urban, C., Berghofer, S., Norrish, M.: Barendregt’s Variable Convention in Rule Inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 35–50. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  27. 27.
    Urban, C., Cheney, J., Berghofer, S.: Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12(2), 15 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Urban, C., Kaliszyk, C.: General Bindings and Alpha-Equivalence in Nominal Isabelle. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 480–500. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • James Cheney
    • 1
  • Christian Urban
    • 2
  1. 1.University of EdinburghUK
  2. 2.TU MunichGermany

Personalised recommendations