Mechanizing the metatheory of mini-XQuery
From MaRDI portal
Recommendations
- A formal and unified description of XML manipulation languages
- scientific article; zbMATH DE number 1696859
- A declarative embedding of XQuery in a functional-logic language
- A core calculus for XQuery 3.0. Combining navigational and pattern matching approaches
- A formal model for an expressive fragment of XSLT
Cites work
- scientific article; zbMATH DE number 2080478 (Why is no real title available?)
- A new approach to abstract syntax with variable binding
- Barendregt’s Variable Convention in Rule Inductions
- Effective interactive proofs for higher-order imperative programs
- Engineering formal metatheory
- Formalising the π-Calculus Using Nominal Logic
- General bindings and alpha-equivalence in Nominal Isabelle
- Mechanizing the metatheory of LF
- Mechanizing the metatheory of mini-XQuery
- Nominal Inversion Principles
- Nominal techniques in Isabelle/HOL
- Parametric higher-order abstract syntax for mechanized semantics
- Regular Expression Subtyping for XML Query and Update Languages
- Static analysis for path correctness of XML queries
- The Abella Interactive Theorem Prover (System Description)
- Theorem Proving in Higher Order Logics
- Toward a verified relational database management system
Cited in
(4)
Describes a project that uses
Uses Software
This page was built for publication: Mechanizing the metatheory of mini-XQuery
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100214)
