In the context of modelling storage, possible worlds refers to a technique of modelling a store in which the allocation of new memory cells is possible through as a Kripke frame.
Concretely, the worlds of the Kripke frame are the store shapes: they specify how many locations there are in the store, and the type of the object they hold.
Accordingly, the accessibility relation specifies that we can reach a store of shape from a store of shape through zero or more allocations.
These models were first proposed by John Reynolds and Frank Oles in the early 1980s, using the language of functor categories.
In many ways such models are now the golden standard. They are often used in combination with step-indexing and realizability models to prove the type-safety of highly expressive languages combining higher-order store and parametric polymophism. A seminal reference for that perspective is Amal Ahmed's 2004 PhD thesis [Ahmed 2004].
Oles, Frank J. 1982. ‘A Category-Theoretic Approach to the Semantics of Programming Languages’. PhD thesis, Syracuse, NY: Syracuse University.
@phdthesis{oles_1982,
address = {Syracuse, NY},
type = {{PhD} thesis},
title = {A {Category}-theoretic {Approach} to the {Semantics} of {Programming} {Languages}},
school = {Syracuse University},
author = {Oles, Frank J.},
year = {1982}
}
Oles, F. J. 1985. ‘Type Algebras, Functor Categories, and Block Structure’. In Algebraic Methods in Semantics, edited by Maurice Nivat and John C. Reynolds, 543–73. Cambridge University Press.
@incollection{oles_1985,
title = {Type {Algebras}, {Functor} {Categories}, and {Block} {Structure}},
booktitle = {Algebraic {Methods} in {Semantics}},
publisher = {Cambridge University Press},
author = {Oles, F. J.},
editor = {Nivat, Maurice and Reynolds, John C.},
year = {1985},
pages = {543--573},
}
This volume is difficult to find, but a prepring is available as an Aarhus tech report:
Oles, Frank J. 1983. ‘Type Algebras, Functor Categories, and Block Structure’. DAIMI Report Series 12 (156). https://doi.org/10.7146/dpb.v12i156.7430.
@article{oles_1983,
title = {Type {Algebras}, {Functor} {Categories}, and {Block} {Structure}},
volume = {12},
url = {https://tidsskrift.dk/daimipb/article/view/7430},
doi = {10.7146/dpb.v12i156.7430},
number = {156},
journal = {DAIMI Report Series},
author = {Oles, Frank J.},
year = {1983}
}
Oles, Frank J. 1997. ‘Functor Categories and Store Shapes’. In Algol-like Languages, edited by Peter W. O’Hearn and Robert D. Tennent, 2:3–12. Boston, MA: Birkhäuser Boston. https://doi.org/10.1007/978-1-4757-3851-3_1.
@incollection{oles_1997,
address = {Boston, MA},
title = {Functor {Categories} and {Store} {Shapes}},
volume = {2},
booktitle = {Algol-like {Languages}},
publisher = {Birkhäuser Boston},
author = {Oles, Frank J.},
editor = {O’Hearn, Peter W. and Tennent, Robert D.},
year = {1997},
doi = {10.1007/978-1-4757-3851-3_1},
pages = {3--12},
}
Ahmed, Amal Jamil. 2004. ‘Semantics of Types for Mutable State’. PhD Thesis, Princeton University. https://www.ccs.neu.edu/home/amal/ahmedsthesis.pdf.
@phdthesis{ahmed_2004,
type = {{PhD} {Thesis}},
title = {Semantics of {Types} for {Mutable} {State}},
url = {https://www.ccs.neu.edu/home/amal/ahmedsthesis.pdf},
school = {Princeton University},
author = {Ahmed, Amal Jamil},
year = {2004}
}