×
Cheney, James; Urban, Christian

Mechanizing the metatheory of mini-XQuery. (English) Zbl 1350.68054

Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 280-295 (2011).
Summary: 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.
For the entire collection see [Zbl 1226.68005].

Cited in 1 Document

MSC:

68N15 Theory of programming languages
68N18 Functional programming and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

XQuery; Isabelle; Abella; CRSX; Isabelle/HOL; Twelf; Nominal Isabelle; PoplMark
PDF BibTeX XML Cite
\textit{J. Cheney} and \textit{C. Urban}, Lect. Notes Comput. Sci. 7086, 280--295 (2011; Zbl 1350.68054)
Full Text: DOI
  • logo of hbz
  • logo of WorldCat

References:

[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) · Zbl 1152.68516
[2] Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL, pp. 3–15 (2008) · Zbl 1295.68052
[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) · Zbl 05597319
[4] Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science 5(2) (2008) · Zbl 1168.68436
[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) · Zbl 1165.68448
[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] Chamberlin, D., Robie, J.: XQuery update facility 1.0. W3C Candidate Recommendation (August 2008), http://www.w3.org/TR/xquery-update-10/
[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) · Zbl 1133.68329
[9] Cheney, J., Urban, C.: Formalization of mini-XQuery in Nominal Isabelle, http://homepages.inf.ed.ac.uk/jcheney/projects/XQuery · Zbl 1350.68054
[10] Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP, pp. 143–156 (2008) · Zbl 1323.68184
[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) · Zbl 1302.68087
[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) · Zbl 1122.68041
[13] Colazzo, D., Sartiani, C.: Precision and complexity of XQuery type inference. In: PPDP (to appear, 2011); Preliminary version in ICTCS 2010
[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) · Zbl 1047.68571
[15] Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002) · Zbl 1001.68083
[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) · Zbl 1165.68457
[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)
[18] Grust, T., Rittinger, J., Teubner, J.: Pathfinder: XQuery off the relational shelf. IEEE Data Eng. Bull. 31(4) (2008)
[19] Hosoya, H., Vouillon, J., Pierce, B.C.: Regular expression types for XML. ACM Trans. Program. Lang. Syst. 27(1), 46–90 (2005) · Zbl 05459284
[20] Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: POPL, pp. 237–248 (2010) · Zbl 1312.68083
[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)
[22] Ré, C., Siméon, J., Fernández, M.F.: A complete and efficient algebraic compiler for XQuery. In: ICDE, p. 14 (2006)
[23] Rose, K.: CRSX - combinatory reduction systems with extensions. In: RTA (2011)
[24] Siméon, J., Wadler, P.: The essence of XML. In: POPL, New York, NY, USA, pp. 1–13. ACM (2003) · Zbl 06481279
[25] Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reasoning 40(4), 327–356 (2008) · Zbl 1140.68061
[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) · Zbl 1213.03024
[27] Urban, C., Cheney, J., Berghofer, S.: Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12(2), 15 (2011) · Zbl 1351.68250
[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) · Zbl 1326.68265
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.