The Unexpurgated Call-by-name, Assignment, and the Lambda-Calculus

Martin Odersky and Dan Rabin

Research Report YALEU/DCS/RR-930
Department of Computer Science, Yale University
May 1993


We define an extension of the call-by-name lambda calculus with
additional constructs and reduction rules that represent mutable
variables and assignments. The extended calculus has neither a concept
of an explicit store nor a concept of evaluation order; nevertheless,
we show that programs in the calculus can be implemented using a
single-threaded store. We also show that the new calculus has the
Church-Rosser property and that it is a conservative extension of
classical lambda calculus with respect to operational equivalence;
that is, all algebraic laws of the functional subset are preserved.