Abstract

Supercompilation is a powerful program transformation technique which can be used to both automatically prove theorems about programs and greatly improve the efficiency with which they execute. Despite its remarkable power, the transformation is simple, principled and fully automatic. Supercompilation is closely related to partial evaluation, but can achieve strictly more optimising transformations.

I intend to give an introduction to supercompilation for those new to the topic, using the framework from our recently accepted Haskell Symposium paper. I will also discuss the difficulties involved in extending the algorithm to a language with recursive let bindings, and how we can use well-known techniques from operational semantics to solve them. Time allowing, I will discuss the surprising issues raised when building supercompilers for a call-by-value language.