Call-by-name, Assignment, and the Lambda-calculus

Martin Odersky, Dan Rabin, Paul Hudak

20th ACM Symposium on Principles of Programming Languages
January 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.