It is a fact that the modelling of store (aka memory) in programming languages is surprisingly difficult.
The history of such models, as well as the state of the art up to the year 2000, are beautifully summarized in [Tennent and Ghica 2000].
The earliest models of a store belong to John McCarthy. We read in [Tennent and Ghica 2000]:
The state of the art in semantic modeling of storage operations before Strachey can be seen in two papers by John McCarthy [23, 24]. Commands in simple imperative languages are modeled as transformations of “state vectors” which are intended to record, among other things, the current values of all program variables. Operations for accessing and updating the current value of any variable are axiomatized.
This is of course sufficient to model global variables.
It should be noted that McCarthy's papers of that time simply plaster over recursion, ignoring the problem. However, modified models of this sort (with a little bit of domain theory to deal with recursion) are often taught in old-fashioned courses on program semantics (e.g. in the 1992 book by Nielson and Nielson).
The next models of stores are due to Christopher Strachey. This work introduced notions such as L- and R-values, storable values, and the higher-order store. This early work is beautifully surveyed in [Tennent and Ghica 2000].
The main problem with these early approaches is that they cannot model any sort of allocation. For example, in any language able to create new storage cells, the program equivalence
is true operationally, but false in the model. Thus, such models are not fully abstract.
In the early 1980s John Reynolds and Frank Oles developed an approach to modelling allocation through possible worlds.
Here, the possible worlds are all the shapes the memory can have. The accessibility relation tells us when the world is reachable from the world through a series of allocations.
Categorically, these models can be thought of as functors from the frame to either sets or (pre)domains.
However, even these models do not validate certain expected equivalences. Two of the most offensive ones are
when does not occur in or , and does not occur in V. Thus, these models are still not fully abstract.
See possible worlds.
Many effects can be modelled as algebraic effects, and this includes storage.
Tennent, Robert D., and Dan R. Ghica. 2000. ‘Abstract Models of Storage’. Higher-Order and Symbolic Computation 13: 119–29. https://doi.org/10.1023/A:1010022312623. [pdf]
@article{tennent_2000,
title = {Abstract {Models} of {Storage}},
volume = {13},
doi = {10.1023/A:1010022312623},
journal = {Higher-Order and Symbolic Computation},
author = {Tennent, Robert D. and Ghica, Dan R.},
year = {2000},
pages = {119--129}
}