TY - GEN
T1 - The parallel intensionally fully abstract games model of PCF
AU - Castellan, Simon
AU - Clairambault, Pierre
AU - Winskel, Glynn
PY - 2015/7/31
Y1 - 2015/7/31
N2 - We describe a framework for truly concurrent game semantics of programming languages, based on Rideau and Winskel's concurrent games on event structures. The model supports a notion of innocent strategy that permits concurrent and non-deterministic behaviour, but which coincides with traditional Hyland-Ong innocent strategies if one restricts to the deterministic sequential case. In this framework we give an alternative interpretation of Plot kin's PCF, that takes advantage of the concurrent nature of strategies and formalizes the idea that although PCF is a sequential language, certain sub-computations are independent and can be computed in a parallel fashion. We show that just as Hyland and Ong's sequential interpretation of PCF, our parallel interpretation yields a model that is intensionally fully abstract for PCF.
AB - We describe a framework for truly concurrent game semantics of programming languages, based on Rideau and Winskel's concurrent games on event structures. The model supports a notion of innocent strategy that permits concurrent and non-deterministic behaviour, but which coincides with traditional Hyland-Ong innocent strategies if one restricts to the deterministic sequential case. In this framework we give an alternative interpretation of Plot kin's PCF, that takes advantage of the concurrent nature of strategies and formalizes the idea that although PCF is a sequential language, certain sub-computations are independent and can be computed in a parallel fashion. We show that just as Hyland and Ong's sequential interpretation of PCF, our parallel interpretation yields a model that is intensionally fully abstract for PCF.
KW - games
KW - semantics
KW - computational modeling
KW - concurrent computing
KW - mathematical modelling
KW - programming language semantics
UR - http://www.scopus.com/inward/record.url?scp=84945897540&partnerID=8YFLogxK
U2 - 10.1109/LICS.2015.31
DO - 10.1109/LICS.2015.31
M3 - Conference contribution book
AN - SCOPUS:84945897540
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 232
EP - 243
BT - Proceedings - 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015
T2 - 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015
Y2 - 6 July 2015 through 10 July 2015
ER -
