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

Frédéric Blanqui 1 Jean-Pierre Jouannaud 2 Albert Rubio 3
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 LSI - Llenguatges i Sistemes Informàtics
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.
keyword : lambda-calculus termination rewriting
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

Vignette du document
main.pdf
Files produced by the author(s)

Identifiers

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

Collections

CNRS | INRIA | LIX | X-LIX | X | LORIA | UNIV-LORRAINE | X-DEP-INFO | INRIA2

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⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

119

Files downloads

180

 

Contact                    Legal Notice                    Personal Data