The computability path ordering: the end of a quest. F. Blanqui, J.-P. Jouannaud and A. Rubio. CSL'08. Invited paper. LNCS 5213.

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.

Statcounter W3C Validator Last updated on 26 November 2015. Come back to main page.