A Game Semantics of Idealized CSP
James D. Laird · Electronic Notes in Theoretical Computer Science · 2001
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.