Coq formalization of the higher-order recursive path ordering
type: Item
instance of: scholarly article
title: Coq formalization of the higher-order recursive path ordering
zbMATH Open document ID: 1185.68628
author: Adam Koprowski
published in: Applicable Algebra in Engineering, Communication and Computing
publication date: 2010-01-18T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5659684
zbMATH Keywords: Coq
zbMATH Keywords: HORPO
zbMATH Keywords: Higher-order rewriting
describes a project that uses: Coq
describes a project that uses: Automath
describes a project that uses: CoLoR
describes a project that uses: PoplMark
MaRDI profile type: Publication
full work available at URL: s00200-009-0105-5
OpenAlex ID: W1998337489
cites work: Q4281462
cites work: Theorem Proving in Higher Order Logics
cites work: Term Rewriting and All That
cites work: Program extraction from normalization proofs
cites work: Types for Proofs and Programs
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: HORPO with Computability Closure: A Reconstruction
cites work: Q5667469
cites work: A formulation of the simple theory of types
cites work: Certification of Automated Termination Proofs
cites work: An effective proof of the well-foundedness of the multiset path ordering
cites work: Orderings for term-rewriting systems
cites work: What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
cites work: Q3994895
cites work: Q4346206
cites work: Polymorphic higher-order recursive path orderings
cites work: Higher-Order Orderings for Normal Rewriting
cites work: Certified Higher-Order Recursive Path Ordering
cites work: Certification of Proving Termination of Term Rewriting by Matrix Interpretations
cites work: Q3024845
cites work: Proving open properties by induction
cites work: Program extraction from proofs of weak head normalization
cites work: Intensional interpretations of functionals of finite type I
cites work: Q2778883
DOI: 10.1007/S00200-009-0105-5
description: scientific article; zbMATH DE number 5659684