Automated analysis of software code is a fast-evolving field. Termination analysis is probably the most famous aspect, since it corresponds to the halting problem in computability. This undecidable problem is prototypical of an interesting phenomenon: though impossible to solve in all generality, in practice, there are powerful methods that frequently succeed in proving termination. Furthermore, recent advances also mean that the resulting tools can provide proofs in a reasonable amount of time--that is, they may soon be practical enough to be a part of one’s standard development toolbox.

Though the problem of (automatically) proving termination of imperative programs still seems quite difficult, the situation for functional programs seems otherwise, as this paper shows. This is likely due to the fact that the invariants in imperative programs more often seem to be arithmetic in nature, while invariants in functional programs are frequently structural. Thus, the latter are rather well suited to the powerful tools developed for proving termination of term rewriting.

This well-written paper has a pleasant pedagogical style that is appropriate for someone who is knowledgeable in the area of programming languages but new to automated termination techniques. The authors formally define, lucidly explain, and motivate various ideas, such as H-termination, termination graphs, termination graph formation rules, and dependency pairs. The authors do an equally good job with the move to higher order and better handling of types. The treatment of type classes, though adequate, does not rise to the same level and appears somewhat overcomplicated.

The paper ends with a set of experiments. While these certainly convey the authors’ message that their techniques--implemented on top of the automated program verification environment (AProVE)--are rather effective, the analysis of the results seems rather shallow. For example, why would it be relevant to report absolute times? As we continue to see rapid changes in this area, wouldn’t the relative time of the analysis to type checking or compilation times be a more appropriate metric? It is disconcerting to read that a 94-node graph is considered large, while most compiler writers would consider a 10,000-line program to be medium sized.

Particularly intriguing is how much their rules resemble similar rules in partial evaluation and supercompilation. The key rule, instantiation, corresponds to generalization in partial evaluators; however, the set of heuristics used in both cases seems to be quite different. There might be an opportunity for further research in that area. Similarly, it is very natural to consider the relation between this analysis and abstract interpretation. The two are naturally related, but the details might be rather instructive.

Anyone interested in automated analysis of functional programs would benefit from reading this paper, whether or not they are interested in termination analysis or Haskell in particular.