Termination is a desirable property of a program
transformer: be it a partial evaluation, specializer or supercompiler.
It is often hard to prove that a transformer indeed terminates. In this
talk we will present a language-independent framework for proving
termination of program transformers. We will also discuss some
techniques to ensure termination and apply the framework to
State University, Stary Peterhof, Universitetski pr., 28