The computability path ordering: The end of a quest
International Workshop on Computer Science Logic, 2008•Springer
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 à la Tait and Girard,
therefore explaining the name of the improved ordering.
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 à la Tait and Girard,
therefore explaining the name of the improved ordering.
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 à la Tait and Girard, therefore explaining the name of the improved ordering.
Springer