Mechanizing the Metatheory of mini-XQuery (Q3100214): Difference between revisions

@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nominal Isabelle
@@ Property / describes a project that uses: Nominal Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CRSX
@@ Property / describes a project that uses: CRSX / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+XQuery
@@ Property / describes a project that uses: XQuery / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-25379-9_21
+Normal rank
@@ Property / OpenAlex ID @@
+W2287532540
@@ Property / OpenAlex ID: W2287532540 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+Formalising the π-Calculus Using Nominal Logic
@@ Property / cites work: Formalising the π-Calculus Using Nominal Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal Inversion Principles
@@ Property / cites work: Nominal Inversion Principles / rank @@
+Normal rank
@@ Property / cites work @@
+Regular Expression Subtyping for XML Query and Update Languages
+Normal rank
@@ Property / cites work @@
+Mechanizing the Metatheory of mini-XQuery
@@ Property / cites work: Mechanizing the Metatheory of mini-XQuery / rank @@
+Normal rank
@@ Property / cites work @@
+Parametric higher-order abstract syntax for mechanized semantics
+Normal rank
@@ Property / cites work @@
+Effective interactive proofs for higher-order imperative programs
+Normal rank
@@ Property / cites work @@
+Static analysis for path correctness of XML queries
+Normal rank
@@ Property / cites work @@
+Q4473276
@@ Property / cites work: Q4473276 / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+The Abella Interactive Theorem Prover (System Description)
+Normal rank
@@ Property / cites work @@
+Toward a verified relational database management system
+Normal rank
@@ Property / cites work @@
+Nominal techniques in Isabelle/HOL
@@ Property / cites work: Nominal techniques in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Barendregt’s Variable Convention in Rule Inductions
+Normal rank
@@ Property / cites work @@
+Mechanizing the metatheory of LF
@@ Property / cites work: Mechanizing the metatheory of LF / rank @@
+Normal rank
@@ Property / cites work @@
+General Bindings and Alpha-Equivalence in Nominal Isabelle
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:3100214