The "size-change" approach to detecting program termination (reported at POPL 2001) is easily automated, and fairly general in that it can, without special treatment, handle programs with permuted parameters and mutual recursion. Its computational aspects are well-understood: The analysis itself has worst-case PSPACE complexity but seems to work well in practice. As to the method's power, a function is computable by a size-change terminating program iff it is multiple recursive (in the sense of R. Peter).
A weakness of the POPL'01 approach is that it seems inherently limited to first-order programs. This lecture will describe ongoing work (joint with N. Bohr) to develop a "size-change" termination analysis for higher-order programs. The question of "what decreases?" in a lambda calculus evaluation has a very operational answer in our approach: The size of the "closures" traditionally used to represent functions as values.