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

Authors:

Martin Odersky, Dan Rabin, and Paul Hudak

Abstract:

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 singlethreaded 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.

Bibtex:

 @InProceedings{ORH-93,
  author = 	"Martin Odersky and Dan Rabin and Paul Hudak",
  title = 	"Call-by-name, Assignment, and the Lambda Calculus",
  booktitle =	{Proceedings of the Twentieth Annual {ACM} Symposium
                 on Principles of Programming Languages, Charleston,
                 South Carolina},
  pages =	"43-57",
  year = 	"1993",
  month = 	"January"
} 

Links:

CBN-Ass-LC-POPL93.pdf