We present a calculus that captures the operational semantics of
The call-by-need lambda calculus is confluent, has a notion of standard
reduction, and entails the same
observational equivalence relation as the call-by-name calculus. The system
can be formulated
with or without explicit let bindings, admits useful notions of marking
and has a straightforward operational interpretation.