Copenhagen Programming Language Seminar


Termination Analysis of the Untyped Lambda Calculus

Neil D. Jones
DIKU, University of Copenhagen
Computer Science Department

Thursday, December 11th, 15:15-16:00
ITU, Glentevej 67, room 2.03


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.

Scientific host: Andrzej Filinski. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org