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.
CITATION STYLE
Blanqui, F., Jouannaud, J.-P., & Rubio, A. (2008). The Computability Path Ordering: The End of a Quest (pp. 1–14). https://doi.org/10.1007/978-3-540-87531-4_1
Mendeley helps you to discover research relevant for your work.