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 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.
In this paper, we give a graph-based definition of the distillation transformation algorithm. This definition is made within a similar framework to the positive supercompilation algorithm, thus allowing for a more in-depth ...
Proofs involving infinite structures can use corecursive functions
as inhabitants of a corecursive type. Admissibility of such functions
in theorem provers such as Coq or Agda, requires that these functions are
productive. ...
In this paper, we give a re-formulation of our previously defined distillation algorithm, which can automatically transform higherorder functional programs into equivalent tail-recursive programs. Our
re-formulation ...
In this paper, we describe a hierarchy of program transformers
in which the transformer at each level of the hierarchy builds on top of
the transformers at lower levels. The program transformer at the bottom
of the ...
Program transformation is a popular technique for attempting
to improve the e ciency of a program. At a high level, program transformation
is the process of taking an input program and transforming
it into an improved ...
