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 <>
Submitted on : Monday, August 27, 2007 - 12:21:26 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
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

315

Files downloads

505