HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

HORPO with Computability Closure : A Reconstruction

Abstract : This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.
Document type :
Conference papers
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/inria-00168304
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Monday, August 27, 2007 - 12:21:26 PM
Last modification on : Friday, February 4, 2022 - 3:30:27 AM
Long-term archiving on: : Friday, April 9, 2010 - 1:10:38 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00168304, version 1
  • ARXIV : 0708.3582

Collections

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio. HORPO with Computability Closure : A Reconstruction. 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Oct 2007, Yerevan, Armenia. ⟨inria-00168304⟩

Share

Metrics

Record views

119

Files downloads

180