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 - http://www.scopus.com/inward/record.url?scp=18944391908&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1016/S1571-0661(04)80965-4
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 -