The following technical report is available from http://aib.informatik.rwth-aachen.de/:

Klaus Indermark, Thomas Noll:

Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information 2004-8

Abstract: Adding appropriate strictness information to recursive function definitions we achieve a uniform treatment of lazy and eager evaluation strategies. By restriction to first-order functions over basic types we develop a pure stack implementation that avoids a heap even for lazy arguments. We present algebraic definitions of denotational, operational, and stack-machine semantics and prove their equivalence by means of structural induction.

Regards, Volker