Higher-Order Termination: from Kruskal to Computability

Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In computer science, termination has always been an important issue for showing programs correct. In this article, we show how the "computability predicate" method of Tait and Girard can be used to build powerful termination orderings for both first-order and higher-order rewriting.