Supercompilation and normalisation by evaluation

peer-reviewedIt has been long recognised that partial evaluation is related to proof normalisation. Normalisation by evaluation, which has been presented for theories with simple types, has made this correspondance formal. Recently Andreas Abel formalised an algorithm for normalisation by evaluation for System F. This is an important step towards the use of such techniques on practical functional programming languages such as Haskell which can reasonably be embedded in relatives of System F?. Supercompilation is a program transformation technique which performs a superset of the simplications performed by partial evaluation. The focus of this paper is to formalise the relationship between supercompilation and normalisation by evaluation