Coq formalization of the higher-order recursive path ordering (Q843949): Difference between revisions

@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / 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/s00200-009-0105-5
+Normal rank
@@ Property / OpenAlex ID @@
+W1998337489
@@ Property / OpenAlex ID: W1998337489 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281462
@@ Property / cites work: Q4281462 / 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 @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Program extraction from normalization proofs
@@ Property / cites work: Program extraction from normalization proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / 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 @@
+HORPO with Computability Closure: A Reconstruction
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Certification of Automated Termination Proofs
@@ Property / cites work: Certification of Automated Termination Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+An effective proof of the well-foundedness of the multiset path ordering
+Normal rank
@@ Property / cites work @@
+Orderings for term-rewriting systems
@@ Property / cites work: Orderings for term-rewriting systems / rank @@
+Normal rank
@@ Property / cites work @@
+What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4346206
@@ Property / cites work: Q4346206 / rank @@
+Normal rank
@@ Property / cites work @@
+Polymorphic higher-order recursive path orderings
@@ Property / cites work: Polymorphic higher-order recursive path orderings / rank @@
+Normal rank
@@ Property / cites work @@
+Higher-Order Orderings for Normal Rewriting
@@ Property / cites work: Higher-Order Orderings for Normal Rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+Certified Higher-Order Recursive Path Ordering
@@ Property / cites work: Certified Higher-Order Recursive Path Ordering / rank @@
+Normal rank
@@ Property / cites work @@
+Certification of Proving Termination of Term Rewriting by Matrix Interpretations
+Normal rank
@@ Property / cites work @@
+Q3024845
@@ Property / cites work: Q3024845 / rank @@
+Normal rank
@@ Property / cites work @@
+Proving open properties by induction
@@ Property / cites work: Proving open properties by induction / rank @@
+Normal rank
@@ Property / cites work @@
+Q2852349
@@ Property / cites work: Q2852349 / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Q2778883
@@ Property / cites work: Q2778883 / rank @@
+Normal rank