Supercompilation and normalisation by evaluation

Abstract. It has been long recognised that partial evaluation is related to proof normalisation. Normalisation by evaluation, which has been pre-sented for theories with simple types, has made this correspondance for-mal. 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ω. Su-percompilation 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.