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