Algebraic Correctness Proofs for Compiling Recursive Function Definitions
with Strictness Information

Klaus Indermark, Thomas Noll

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.