A graphical foundation for schedules

Guy McCusker, John Power, Cai Wingfield

Research output: Contribution to journalArticle

  • 24 Citations

Abstract

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.
LanguageEnglish
Pages273-289
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume286
DOIs
StatusPublished - 24 Sep 2012

Fingerprint

Schedule
Chemical analysis
Semantics
Game Semantics
Associativity
Geometry
Graphics
Formulation

Cite this

A graphical foundation for schedules. / McCusker, Guy; Power, John; Wingfield, Cai.

In: Electronic Notes in Theoretical Computer Science, Vol. 286, 24.09.2012, p. 273-289.

Research output: Contribution to journalArticle

@article{a77c3492c64e4477bb45bf497a8869c6,
title = "A graphical foundation for schedules",
abstract = "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.",
author = "Guy McCusker and John Power and Cai Wingfield",
note = "Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII)",
year = "2012",
month = "9",
day = "24",
doi = "10.1016/j.entcs.2012.08.018",
language = "English",
volume = "286",
pages = "273--289",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

TY - JOUR

T1 - A graphical foundation for schedules

AU - McCusker,Guy

AU - Power,John

AU - Wingfield,Cai

N1 - Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII)

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.

UR - http://www.scopus.com/inward/record.url?scp=84856203520&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1016/j.entcs.2012.08.018

U2 - 10.1016/j.entcs.2012.08.018

DO - 10.1016/j.entcs.2012.08.018

M3 - Article

VL - 286

SP - 273

EP - 289

JO - Electronic Notes in Theoretical Computer Science

T2 - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -