Marked store models

Marked store models are an early technique for modelling a first-order store that has the ability to allocate fresh variables. They do so by imitating the implementation: memory allocation is modelled by systematically picking an uninitialized location.

Marked store models are not pleasant to work with mathematically. They have been almost completely replaced by models based on functor categories or nominal sets.

Example

There are many ways to express the same idea. The example here comes from Sieber 1996.

Let \mathsf{Loc} be an infinite set of locations. Assume we have a function

  \textsf{next} : \mathcal{P}_\text{fin}(\textsf{Loc}) \to \textsf{Loc}

which, for each finite set of 'locations currently in use' S returns a fresh, unusued location \textsf{next}(S) \not\in S.

A marked store is then a finite function

  m : \textsf{Loc} \rightharpoonup_\textsf{fin} \mathbb{N}

Its finite domain dom(m) is the locations marked as active.
m(\ell) are the contents of location \ell (if defined)
\textsf{next}(dom(m)) is the next free location to be allocated next.

References

The following classic books on denotational semantics contain descriptions of marked store models:

J. de Bakker, Mathematical Theory of Program Correctness, International Series in Computer Science (Prentice Hall, Englewood Cliffs, NJ, 1980).

M.J.C. Gordon, The Denotational Description of Programming Languages (Springer, Berlin, 1979).

H.R. Nielson and F. Nielson, Semantics with Applications: A Formal Introduction (Wiley Professional Computing, Wiley, New York, 1992).

Some of this bibliography and the example come from

Sieber, Kurt. 1996. ‘Full Abstraction for the Second Order Subset of an Algol-like Language’. Theoretical Computer Science 168 (1): 155–212. https://doi.org/10.1016/S0304-3975(96)00066-7.

@article{sieber_full_1996,
	title = {Full abstraction for the second order subset of an {Algol}-like language},
	volume = {168},
	doi = {10.1016/S0304-3975(96)00066-7},
	number = {1},
	journal = {Theoretical Computer Science},
	author = {Sieber, Kurt},
	year = {1996},
	pages = {155--212},
	annote = {This is the JOURNAL version of the article from 1994. “Algol-like languages” contains the conference version.}
}