Projects per year
Abstract
In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notion they called a {multimap}schedule, and the similar notion of ⊗schedule, both structures describing interleavings of plays in games. Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice. Moreover, several proofs of key properties, such as that the composition of {multimap}schedules is associative, involve cumbersome combinatorial detail, whereas in terms of pictures the proof is straightforward, reflecting the geometry of the plane. Here, we give a geometric formulation of {multimap}schedules and ⊗schedules, prove that they are isomorphic to Harmer et al.'s definitions, and illustrate their value by giving such geometric proofs. Harmer et al.'s notions may be combined to describe plays in multicomponent games, and researchers have similarly developed intuitive graphical representations of plays in these games. We give a characterisation of these diagrams and explicitly describe how they relate to the underlying schedules, finally using this relation to provide new, intuitive proofs of key categorical properties.
Original language  English 

Pages (fromto)  11311174 
Number of pages  44 
Journal  Journal of Pure and Applied Algebra 
Volume  219 
Issue number  4 
Early online date  9 Jun 2014 
DOIs  
Publication status  Published  1 Apr 2015 
Keywords
 game semantics, geometry, schedules, composites, associativity, symmetric monoidal closed category
Fingerprint Dive into the research topics of 'A graphical foundation for interleaving in game semantics'. Together they form a unique fingerprint.
Projects
 1 Finished

Coalgebraic Logic Programming for Type Inference
Power, J.
Engineering and Physical Sciences Research Council
1/09/13 → 31/01/17
Project: Research council