Programming Inductive Proofs (Q3058448): Difference between revisions

@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Elf
@@ Property / describes a project that uses: Elf / 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 @@
+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-17172-7_1
+Normal rank
@@ Property / OpenAlex ID @@
+W197201650
@@ Property / OpenAlex ID: W197201650 / 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 @@
+Explicit substitutions
@@ Property / cites work: Explicit substitutions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281462
@@ Property / cites work: Q4281462 / rank @@
+Normal rank
@@ Property / cites work @@
+A verified compiler for an impure functional language
+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 @@
+Q3024905
@@ Property / cites work: Q3024905 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
+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 @@
+Towards a mechanized metatheory of standard ML
@@ Property / cites work: Towards a mechanized metatheory of standard ML / rank @@
+Normal rank
@@ Property / cites work @@
+A formally verified compiler back-end
@@ Property / cites work: A formally verified compiler back-end / rank @@
+Normal rank
@@ Property / cites work @@
+Contextual modal type theory
@@ Property / cites work: Contextual modal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+Q4012879
@@ Property / cites work: Q4012879 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying termination and reduction properties about higher-order logic programs
+Normal rank
@@ Property / cites work @@
+Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
+Normal rank
@@ Property / cites work @@
+A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
+Normal rank