Refining First-Class Stores
J. Gregory Morrisett


A first-class store is an object that captures the values of mutable
objects at a particular time in a program's execution.  First-class
stores allow programmers to cleanly, safely, and efficiently implement
"undo" and "redo" operations on mutable objects.  This paper describes
a generalized interface for first-class stores that allows the
programmer to partition mutable data and refine the scope of store
objects.  We demonstrate the power of the interface by discussing
three applications: version arrays, replay debugging, and nested
transactions.  A denotational semantics for first-class stores is
given and two implementations are discussed.