Offline partial evaluation techniques rely on an annotated version of the source program to control the specialisation process. These annotations guide the specialisation and have to ensure termination of the partial evaluation. We present an algorithm for generating these annotations automatically. The algorithm uses state-of-the-art termination analysis techniques, combined with a new type-based abstract interpretation for propagating the binding types. This algorithm has been implemented as part of the logen partial evaluation system, and we report on performance of the algorithm on a series of benchmarks.
Stephen-John Craig, John P. Gallagher, Michael Leu