BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Semantics of Full Ground References - Paul Blain Levy (University 
 of Birmingham)
DTSTART:20170721T130000Z
DTEND:20170721T140000Z
UID:TALK73119@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:"Full ground references" means references to integers and to o
 ther\nreferences\, but not to functions or thunks\, Murawski and Tzeveleko
 s\nprovided game semantics for this language feature\, using strong nomina
 l\nsets.\n\nThe first part of the talk gives Kripke semantics for call-by-
 push-value\nwith full ground references.  (I will briefly introduce\ncall-
 by-push-value.)  The key idea is that a computation type's\ndenotation is 
 a semantic domain for configurations consisting of some\nextra local cells
 \, a state and a computation.  These are functorial in\ntwo ways\, corresp
 onding to injective renaming of global cells\, with\ninitiailzation\, and 
 hiding of global cells.\n\nThe second part of our talk zooms in on the fir
 st order fragment of the\nlanguage\, and explains how a stateful value col
 lection can be\nrepresented as a finitely supported path through the so-ca
 lled "heap\npossibliity graph".   This has the potential to simplify both 
 the Kripke\nand the game semantics.\n\nNote: this work is joint with Ohad 
 Kammar\, Sean Moss and Sam Staton.\nOhad gave an overlapping talk in Cambr
 idge in February.  This talk is\ncomplementary for people who attended tha
 t talk and self-contained for\npeople who didn't.
LOCATION:FW26
END:VEVENT
END:VCALENDAR