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.