Journal of Functional Programming

The call-by-need lambda calculus

a1 School of Computer and Information Science, University of South Australia, Warrendi Road, The Levels, Adelaide, SA 5095, Australia; e-mail:
a2 Bell Laboratories, Lucent Technologies, 700 Mountain Ave., Room 2T-304, Murray Hill, NJ 07974-0636, USA; e-mail:


We present a calculus that captures the operational semantics of call-by-need. 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 developments, and has a straightforward operational interpretation.