"A Call-by-Need Lambda Calculus"

Zena Ariola, Matthias Felleisen, John Maraist,
	Martin Odersky and Philip Wadler.

Proc. 22nd ACM Symposium on Principles of Programming Languages

Abstract: 
The mismatch between the operational semantics of the lambda calculus
and the actual behavior of implementations is a major obstacle for
compiler writers. They cannot explain the behavior of their evaluator
in terms of source level syntax, and they cannot easily compare
distinct implementations of different lazy strategies.  In this paper
we derive an equational characterization of call-by-need and prove it
correct with respect to the original lambda calculus.  The theory is a
strictly smaller theory than the lambda calculus.  Immediate
applications of the theory concern the correctness proofs of a number
of implementation strategies, e.g., the call-by-need continuation
passing transformation and the realization of sharing via assignments.