Semantics of Full Ground References

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

• Paul Blain Levy (University of Birmingham)
• Friday 21 July 2017, 14:00-15:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.