The Computability Path Ordering: The End of a Quest

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.

• Type: Conference
• Year: 2008
• Where: CSL
• Authors: Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
• Keywords: Automated Reasoning, Computability Path, CSL 2008, Path Ordering, Survey Automated Termination