A language with a store behaves very differently depending on what is a storable value.
Many languages have a first-order store, in which only first-order values may be stored (e.g. integers, booleans, strings).
Functional languages often have a higher-order store, in which entire functions can be placed (represented as closures).
However, there is also an intermediate situation, in which a language may just store full ground references. This includes first-order values such as integers and booleans, but also addresses to other memory locations.
A model of full ground references based on game semantics is given by [Murawski and Tzevelekos 2012, 2018].
A model given by a monad on an Oles model is given by [Kammar et al. 2017]. This allows types generated by the following grammar as storable values:
where is a cell sort drawn from a set . The content type of a cell is given by a sorting function assigning a full ground reference to each sort. The pair is referred to as a full ground storage signature; this corresponds to a sequence of top-level data declarations, and remains fixed.
A BI hyperdoctrine structure for reasoning over this model is given by [Polzer and Goncharov 2020].
Murawski, Andrzej S., and Nikos Tzevelekos. 2012. ‘Algorithmic Games for Full Ground References’. In Automata, Languages, and Programming, edited by Artur Czumaj, Kurt Mehlhorn, Andrew Pitts, and Roger Wattenhofer, 7392:312–24. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_30. [pdf]
@inproceedings{murawski_2012,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Algorithmic {Games} for {Full} {Ground} {References}},
volume = {7392},
doi = {10.1007/978-3-642-31585-5_30},
booktitle = {Automata, {Languages}, and {Programming}},
publisher = {Springer Berlin Heidelberg},
author = {Murawski, Andrzej S. and Tzevelekos, Nikos},
editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew and Wattenhofer, Roger},
year = {2012},
pages = {312--324}
}
The same paper appeared in Formal Methods in System Design in 2018:
Murawski, Andrzej S., and Nikos Tzevelekos. 2018. ‘Algorithmic Games for Full Ground References’. Formal Methods in System Design 52 (3): 277–314. https://doi.org/10.1007/s10703-017-0292-9. [pdf]
@article{murawski_algorithmic_2018,
title = {Algorithmic games for full ground references},
volume = {52},
doi = {10.1007/s10703-017-0292-9},
number = {3},
journal = {Formal Methods in System Design},
author = {Murawski, Andrzej S. and Tzevelekos, Nikos},
year = {2018},
pages = {277--314}
}
Kammar, Ohad, Paul B. Levy, Sean K. Moss, and Sam Staton. 2017. ‘A Monad for Full Ground Reference Cells’. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–12. Reykjavik, Iceland: IEEE. https://doi.org/10.1109/LICS.2017.8005109. [pdf] [arXiv]
@inproceedings{kammar_monad_2017,
address = {Reykjavik, Iceland},
title = {A monad for full ground reference cells},
doi = {10.1109/LICS.2017.8005109},
booktitle = {2017 32nd {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science} ({LICS})},
publisher = {IEEE},
author = {Kammar, Ohad and Levy, Paul B. and Moss, Sean K. and Staton, Sam},
year = {2017}
}
Polzer, M., Goncharov, S. (2020). Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science, vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_28