|
 |
|
|||||||||||
|
|
|
|
|||||||||||
|
|
Supercompilation and Normalisation By Evaluation Gavin Mendel-Gleason and Geoff Hamilton,
It 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 correspondence 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 simplifications performed by partial evaluation. The focus of this paper is to formalise the relationship between supercompilation and normalisation by evaluation for System F with recursive types and terms.
|
