University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Semantics of Full Ground References

Semantics of Full Ground References

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dominic Mulligan.

“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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity