The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-015-9327-3
@@ Property / DOI: 10.1007/s10817-015-9327-3 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Vellvm
@@ Property / describes a project that uses: Vellvm / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Beluga
@@ Property / describes a project that uses: Beluga / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Toolchain
@@ Property / describes a project that uses: Toolchain / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HYBRID
@@ Property / describes a project that uses: HYBRID / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / 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/s10817-015-9327-3
+Normal rank
@@ Property / OpenAlex ID @@
+W1551936078
@@ Property / OpenAlex ID: W1551936078 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: Abella Formalization of λ-Calculus Cube Property
+Normal rank
@@ Property / cites work @@
+Cut elimination for a logic with induction and co-induction
+Normal rank
@@ Property / cites work @@
+Verified Software Toolchain
@@ Property / cites work: Verified Software Toolchain / rank @@
+Normal rank
@@ Property / cites work @@
+On the Expressivity of Minimal Generic Quantification
+Normal rank
@@ Property / cites work @@
+Q4012875
@@ Property / cites work: Q4012875 / rank @@
+Normal rank
@@ Property / cites work @@
+Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
+Normal rank
@@ Property / cites work @@
+Programming with binders and indexed data-types
@@ Property / cites work: Programming with binders and indexed data-types / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit Contexts in LF (Extended Abstract)
@@ Property / cites work: Explicit Contexts in LF (Extended Abstract) / rank @@
+Normal rank
@@ Property / cites work @@
+Case Analysis of Higher-Order Data
@@ Property / cites work: Case Analysis of Higher-Order Data / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
+Normal rank
@@ Property / cites work @@
+Q4484341
@@ Property / cites work: Q4484341 / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
+Normal rank
@@ Property / cites work @@
+The Abella Interactive Theorem Prover (System Description)
+Normal rank
@@ Property / cites work @@
+Reasoning with higher-order abstract syntax in a logical framework
+Normal rank
@@ Property / cites work @@
+Nominal abstraction
@@ Property / cites work: Nominal abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+A two-level logic approach to reasoning about computations
+Normal rank
@@ Property / cites work @@
+Verifying termination and reduction properties about higher-order logic programs
+Normal rank
@@ Property / cites work @@
+Mechanizing metatheory in a logical framework
@@ Property / cites work: Mechanizing metatheory in a logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Programming with Higher-Order Logic
@@ Property / cites work: Programming with Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4417871
@@ Property / cites work: Q4417871 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2844810
@@ Property / cites work: Q2844810 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2871875
@@ Property / cites work: Q2871875 / rank @@
+Normal rank
@@ Property / cites work @@
+Contextual modal type theory
@@ Property / cites work: Contextual modal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
+Normal rank
@@ Property / cites work @@
+Programming Inductive Proofs
@@ Property / cites work: Programming Inductive Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q5277845
@@ Property / cites work: Q5277845 / rank @@
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+The Twelf Proof Assistant
@@ Property / cites work: The Twelf Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Q4249901
@@ Property / cites work: Q4249901 / rank @@
+Normal rank
@@ Property / cites work @@
+A Coverage Checking Algorithm for LF
@@ Property / cites work: A Coverage Checking Algorithm for LF / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing the LLVM intermediate representation for verified program transformations
+Normal rank
@@ Property / DOI @@
+.1007/S10817-015-9327-3
@@ Property / DOI: 10.1007/S10817-015-9327-3 / rank @@
+Normal rank