TY - JOUR

T1 - A graphical foundation for schedules

AU - McCusker, Guy

AU - Power, John

AU - Wingfield, Cai

PY - 2012/9/24

Y1 - 2012/9/24

N2 - In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notion they called a schedule. Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice. Moreover, a proof that the composition of schedules is associative involves 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 schedule, prove that it is equivalent to Harmer et al.ʼs definition, and illustrate its value by giving a proof of associativity of composition.

AB - In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notion they called a schedule. Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice. Moreover, a proof that the composition of schedules is associative involves 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 schedule, prove that it is equivalent to Harmer et al.ʼs definition, and illustrate its value by giving a proof of associativity of composition.

KW - Game semantics

KW - geometry

KW - schedules

KW - composites

KW - associativity

U2 - 10.1016/j.entcs.2012.08.018

DO - 10.1016/j.entcs.2012.08.018

M3 - Journal article

VL - 286

SP - 273

EP - 289

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -