The computability path ordering: the end of a quest
classification
💻 cs.LO
keywords
orderingcomputabilitypathdefinitionhigher-orderimprovedappearsarguments
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.