Abstract

“Full ground references” means references to integers and to other references, but not to functions or thunks, Murawski and Tzevelekos provided game semantics for this language feature, using strong nominal sets.

The first part of the talk gives Kripke semantics for call-by-push-value with full ground references. (I will briefly introduce call-by-push-value.) The key idea is that a computation type’s denotation is a semantic domain for configurations consisting of some extra local cells, a state and a computation. These are functorial in two ways, corresponding to injective renaming of global cells, with initiailzation, and hiding of global cells.

The second part of our talk zooms in on the first order fragment of the language, and explains how a stateful value collection can be represented as a finitely supported path through the so-called “heap possibliity graph”. This has the potential to simplify both the Kripke and the game semantics.

Note: this work is joint with Ohad Kammar, Sean Moss and Sam Staton. Ohad gave an overlapping talk in Cambridge in February. This talk is complementary for people who attended that talk and self-contained for people who didn’t.