Termination Analysis of Higher-Order Functional Programs

In the Summer School on Program Analysis and Transformation, DIKU, University of Copenhagen, 2005 (PAT 2005).

Authors

Damien Sereni and Neil D. Jones.

Abstract

Size-change termination (SCT) automatically identifies termination of first-order functional programs. The SCT principle: a program terminates if every infinite control flow sequence would cause an infinite descent in a well-founded data value (POPL 2001).

More recent work (RTA 2004) developed a termination analysis of the pure untyped lambda-calculus using a similar approach, but an entirely different notion of size was needed to compare higher-order values. Again this is a powerful analysis, even proving termination of certain lambda-expressions containing the fixpoint combinator Y. However the language analysed is tiny, not even containing constants.

These techniques are unified and extended significantly, to yield a termination analyser for higher-order, call-by-value programs as in ML's purely functional core or similar functional languages. Our analyser has been proven correct, and implemented for a substantial subset of OCaml.

Electronic Copy

An improved version of these notes were published in APLAS 2005.

BIBTEX

  @inproceedings{pat05sereni, 
    author = "Damien Sereni and Neil D. Jones", 
    title = "Termination Analysis of Higher-Order Functional Programs", 
    booktitle = "Summer School on Program Analysis and Transformation (PAT 2005)", 
    year = "2005"}