Reasoning in Abella about Structural Operational Semantics Specifications (Q2804943): Difference between revisions

@@ Property / DOI @@
-.1016/j.entcs.2008.12.118
@@ Property / DOI: 10.1016/j.entcs.2008.12.118 / rank @@
-Normal rank
@@ 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 @@
+Teyjus
@@ Property / describes a project that uses: Teyjus / 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.1016/j.entcs.2008.12.118
+Normal rank
@@ Property / OpenAlex ID @@
+W2119790470
@@ Property / OpenAlex ID: W2119790470 / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+The Abella Interactive Theorem Prover (System Description)
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Logic programming in a fragment of intuitionistic linear logic
+Normal rank
@@ Property / cites work @@
+Unification under a mixed prefix
@@ Property / cites work: Unification under a mixed prefix / rank @@
+Normal rank
@@ Property / cites work @@
+Forum: A multiple-conclusion specification logic
@@ Property / cites work: Forum: A multiple-conclusion specification logic / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning with higher-order abstract syntax in a logical framework
+Normal rank
@@ Property / cites work @@
+Uniform proofs as a foundation for logic programming
+Normal rank
@@ Property / cites work @@
+A proof theory for generic judgments
@@ Property / cites work: A proof theory for generic judgments / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q2871867
@@ Property / cites work: Q2871867 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Q2871856
@@ Property / cites work: Q2871856 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / DOI @@
+.1016/J.ENTCS.2008.12.118
@@ Property / DOI: 10.1016/J.ENTCS.2008.12.118 / rank @@
+Normal rank