PLS Lab

Full ground references

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.

Models

Game semantics

A model of full ground references based on game semantics is given by Murawski and Tzevelekos 2012, 2018.

Oles models

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:

	\sigma \in \mathbb{T} \Coloneqq
  			 \mathbf{0}
    \mid \mathbf{1}
    \mid \sigma + \sigma
    \mid \sigma \times \sigma
    \mid \textbf{ref}_c

where c is a cell sort drawn from a set \mathbf{S}. The content type of a cell \textbf{ref}_c is given by a sorting function ctype : \mathbf{S} \to \mathbb{T} assigning a full ground reference to each sort. The pair (\mathbf{S}, ctype) 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.

References

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

Springer

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