Possible worlds (storage)

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 w \in \mathcal{W} 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 w \sqsubseteq w' specifies that we can reach a store of shape w' from a store of shape w 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.

References

Possible world models for the store first appeared in Frank Oles' 1982 PhD thesis:

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}
}

A short description of the method was printed as

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}
}

A version of the same text that has been adapted is reprinted in the 2nd Algol-like languages volume:

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},
}

A modern approach to possible world semantics for storage without any categorical machinery is given in Amal Ahmed's 2004 PhD thesis:

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}
}

Possible worlds (storage)

See also

References