Improvement Theory and its Applications

An improvement theory is a variant of the standard theories of observational approximation (or equivalence) in which the basic observations made of a functional program’s execution include some intensionalinformation about, for example, the program’s computational cost. One program is an improvement of another if its execution is more efficient in any program context. In this article we give an overview of our work on the theory and applications of improvement. Applications include reasoning about time properties of functional programs, and proving the correctness of program transformation methods. We also introduce a new application, in the form of some bisimulationlike proof techniques for equivalence, with something of the flavour of Sangiorgi’s “bisimulation up-to expansion and context”