A graphical foundation for schedules

Guy McCusker, John Power, Cai Wingfield

OAI: oai:purehost.bath.ac.uk:openaire_cris_publications/a77c3492-c64e-4477-bb45-bf497a8869c6 • DOI: https://doi.org/10.1016/j.entcs.2012.08.018

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.