A game semantics of idealized CSP

J. Laird

doi:10.1016/S1571-0661(04)80965-4

A game semantics of idealized CSP

J. Laird

Research output: Contribution to journal › Article › peer-review

19 Citations (SciVal)

Abstract

A games semantics is described for a typed functional language which includes primitives for parallel composition and for synchronous communication on private channels. The semantics is based on a category obtained by extending "Hyland-Ong games" with a representation of multiple threads of control using "concurrency pointers" which express a new kind of causality relation between moves. The semantics is proved to be fully abstract for "channel-free" types with respect to a may-and-must equivalence for the finitary fragment, and with respect to may-equivalence for the whole language, using factorization results to reduce definability to the sequential case.

Original language	English
Pages (from-to)	232-257
Journal	Electronic Notes in Theoretical Computer Science
Volume	45
DOIs	https://doi.org/10.1016/S1571-0661(04)80965-4
Publication status	Published - Nov 2001

Access to Document

10.1016/S1571-0661(04)80965-4Licence: CC BY-NC-ND

http://dx.doi.org/10.1016/S1571-0661(04)80965-4Licence: CC BY-NC-ND

Cite this

@article{eb738bc7e97144a49a51f86bddbb1407,

title = "A game semantics of idealized CSP",

abstract = "A games semantics is described for a typed functional language which includes primitives for parallel composition and for synchronous communication on private channels. The semantics is based on a category obtained by extending {"}Hyland-Ong games{"} with a representation of multiple threads of control using {"}concurrency pointers{"} which express a new kind of causality relation between moves. The semantics is proved to be fully abstract for {"}channel-free{"} types with respect to a may-and-must equivalence for the finitary fragment, and with respect to may-equivalence for the whole language, using factorization results to reduce definability to the sequential case. ",

author = "J. Laird",

year = "2001",

month = nov,

doi = "10.1016/S1571-0661(04)80965-4",

language = "English",

volume = "45",

pages = "232--257",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - A game semantics of idealized CSP

AU - Laird, J.

PY - 2001/11

Y1 - 2001/11

N2 - A games semantics is described for a typed functional language which includes primitives for parallel composition and for synchronous communication on private channels. The semantics is based on a category obtained by extending "Hyland-Ong games" with a representation of multiple threads of control using "concurrency pointers" which express a new kind of causality relation between moves. The semantics is proved to be fully abstract for "channel-free" types with respect to a may-and-must equivalence for the finitary fragment, and with respect to may-equivalence for the whole language, using factorization results to reduce definability to the sequential case.

AB - A games semantics is described for a typed functional language which includes primitives for parallel composition and for synchronous communication on private channels. The semantics is based on a category obtained by extending "Hyland-Ong games" with a representation of multiple threads of control using "concurrency pointers" which express a new kind of causality relation between moves. The semantics is proved to be fully abstract for "channel-free" types with respect to a may-and-must equivalence for the finitary fragment, and with respect to may-equivalence for the whole language, using factorization results to reduce definability to the sequential case.

UR - https://www.scopus.com/pages/publications/18944391908

UR - http://dx.doi.org/10.1016/S1571-0661(04)80965-4

U2 - 10.1016/S1571-0661(04)80965-4

DO - 10.1016/S1571-0661(04)80965-4

M3 - Article

AN - SCOPUS:18944391908

SN - 1571-0661

VL - 45

SP - 232

EP - 257

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

A game semantics of idealized CSP

Abstract

Access to Document

Other files and links

Fingerprint

Cite this