From global to local state in game semantics via the sequoid

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

• James Laird, University of Bath
• Friday 01 June 2018, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Victor Gomes.

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 procedures,​ coroutines and message-passing between concurrent threads. These are 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 monad is useful, both for understanding the model itself (for example, showing correspondence with the operational semantics) and beyond game semantics, in giving new principles for constructing and reasoning about objects with local state.

To achieve this, we investigate the underlying structure of game semantics using the sequoid, a novel connective which allows us to construct and deconstruct history sensitive strategies. The sequoid A⊘B represents a game in which play in B has some causal dependency in A: it is interpreted as an action of a monoidal category, together with a map in the category of such actions into the canonical action of the monoidal category on itself. We 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 linear logic and CPS . Each imperative effect may be identified with particular categorical properties of the sequoid, which we can use to define equational theories and canonical representations for elements in the corresponding model.

A key example is that in categories of games and history sensitive strategies, a final coalgebra for the functor A⊘_ has the structure of the cofree commutative comonoid on A (giving an interpretation of the “bang” of linear logic). So in particular, if we have a strategy on S 􏰉 􏰉→ (A ⊘ S), corresponding to an object of type A with explicit input and output states of type S (cf. the side-effect monad) we may “encapsulate” its state as a coalgebra morphism S → !A which shares internal state between its threads, and which comes with a corresponding set of coinductive reasoning principles.​

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.