Mechanizing the Metatheory of mini-XQuery
From MaRDI portal
Publication:3100214
DOI10.1007/978-3-642-25379-9_21zbMath1350.68054OpenAlexW2287532540MaRDI QIDQ3100214
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_21
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- A new approach to abstract syntax with variable binding
- Nominal techniques in Isabelle/HOL
- Effective interactive proofs for higher-order imperative programs
- Mechanizing the metatheory of LF
- Mechanizing the Metatheory of mini-XQuery
- Engineering formal metatheory
- The Abella Interactive Theorem Prover (System Description)
- Nominal Inversion Principles
- Barendregt’s Variable Convention in Rule Inductions
- Parametric higher-order abstract syntax for mechanized semantics
- Toward a verified relational database management system
- Regular Expression Subtyping for XML Query and Update Languages
- Theorem Proving in Higher Order Logics
- Static analysis for path correctness of XML queries
- Formalising the π-Calculus Using Nominal Logic
- General Bindings and Alpha-Equivalence in Nominal Isabelle
This page was built for publication: Mechanizing the Metatheory of mini-XQuery
