The computability path ordering: the end of a quest
Logic in Computer Science
2008-12-18 v1
Abstract
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments \`a la Tait and Girard, therefore explaining the name of the improved ordering.
Cite
@article{arxiv.0806.2517,
title = {The computability path ordering: the end of a quest},
author = {Frédéric Blanqui and Jean-Pierre Jouannaud and Albert Rubio},
journal= {arXiv preprint arXiv:0806.2517},
year = {2008}
}
Comments
Dans CSL'08 (2008)