BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From global to local state in game semantics via the sequoid - Jam
 es Laird\, University of Bath
DTSTART:20180601T130000Z
DTEND:20180601T140000Z
UID:TALK103375@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Game semantics has been used to define denotational models of 
 a wide variety of programming languages with stateful effects\, including 
 locally bound integer and general references\, dynamically bound procedure
 s\,​ coroutines and message-passing between concurrent threads. These ar
 e typically given by directly defining the interpretation of key stateful 
 objects (such as reference cells) as “history sensitive” strategies\, 
 for which the whole history of play can act as an internal state. Relating
  these to more explicit representations of state such as the side-effect m
 onad is useful\, both for understanding the model itself (for example\, sh
 owing correspondence with the operational semantics) and beyond game seman
 tics\, in giving new principles for constructing and reasoning about objec
 ts with local state.\n\nTo achieve this\, we investigate the underlying st
 ructure of game semantics using the sequoid\, a novel connective which all
 ows us to construct and  deconstruct history sensitive strategies. The seq
 uoid  A⊘B represents a game in which play in B has some causal dependenc
 y in A: it is interpreted as an action of a monoidal category\, together w
 ith a map in the category of such actions into the canonical action of the
  monoidal category on itself. \nWe may observe sequoidal structure in each
  of the various categories of games which have been used for denotational 
 semantics\, and relate it to other key structuring principles such as  lin
 ear logic and CPS. Each imperative effect may be identified with particula
 r categorical properties of the sequoid\, which we can use to define equat
 ional theories and canonical representations for elements in the correspon
 ding model.\n\nA key example is that in categories of games and history se
 nsitive strategies\, a final coalgebra for the functor A⊘_  has the stru
 cture of the cofree commutative  comonoid on A (giving an interpretation o
 f the “bang” of linear logic). So in particular\, if we have a strateg
 y on  S 􏰉 􏰉→  (A ⊘ S)\, corresponding to an object of type A wit
 h explicit input and output states of type S  (cf. the side-effect monad) 
  we may “encapsulate” its state as a coalgebra morphism S →  !A whic
 h shares internal state between its threads\, and which comes with a corre
 sponding set of coinductive reasoning principles.​
LOCATION:FW26
END:VEVENT
END:VCALENDAR