The parallel intensionally fully abstract games model of PCF

被引:13
作者
Castellan, Simon [1 ]
Clairambault, Pierre [1 ]
Winskel, Glynn [2 ]
机构
[1] Univ Lyon, UCBL, Inria, ENS Lyon,CNRS,LIP, 46 Allee Italie, F-69364 Lyon, France
[2] Univ Cambridge, Comp Lab, Cambridge CB3 0FD, England
来源
2015 30TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2015年
关键词
D O I
10.1109/LICS.2015.31
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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 Plotkin'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.
引用
收藏
页码:232 / 243
页数:12
相关论文
共 19 条
[11]  
Melliès PA, 2005, IEEE S LOG, P386
[12]  
Melliès PA, 2007, LECT NOTES COMPUT SC, V4703, P395
[13]  
Plotkin G. D., 1977, Theoretical Computer Science, V5, P223, DOI 10.1016/0304-3975(77)90044-5
[14]   Concurrent Strategies [J].
Rideau, Silvain ;
Winskel, Glynn .
26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011), 2011, :409-418
[15]  
Wall M.A., 2004, THESIS
[16]  
WINSKEL G, 1986, ADV PETRI NETS, P325, DOI DOI 10.1007/3-540-17906-2_31
[17]  
Winskel G, 2013, LECT NOTES COMPUT SC, V7794, P418, DOI 10.1007/978-3-642-37075-5_27
[18]   Event Structures with Symmetry [J].
Winskel, Glynn .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 172 :611-652
[19]  
Winskel Glynn, 2011, LECT NOTES