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.
There are many ways to express the same idea. The example here comes from [Sieber 1996].
Let be an infinite set of locations. Assume we have a function
which, for each finite set of 'locations currently in use' returns a fresh, unusued location .
A marked store is then a finite function
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).
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.}
}