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 条

[1]

Abramsky S., 1999, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), P431, DOI 10.1109/LICS.1999.782638

[2]

Abramsky S, 2000, INFORM COMPUT, V163, P409, DOI [10.1006/inco.2000.2930, 10.1006/inco2000.2930]

[3]

Castellan Simon, 2014, CSL LICS 14, P28

[4]

Curien Pierre-Louis, 2009, LNCS, V5608

[5] Angelic semantics of fine-grained concurrency [J].

Ghica, Dan R. ;

Murawski, Andrzej S. .

ANNALS OF PURE AND APPLIED LOGIC, 2008, 151 (2-3) :89-114

[6]

Hirschowitz Tom, 2013, Algebra and Coalgebra in Computer Science. 5th International Conference, CALCO 2013. Proceedings: LNCS 8089, P175, DOI 10.1007/978-3-642-40206-7_14

[7] Innocent Strategies as Presheaves and Interactive Equivalences for CCS [J].

Hirschowitz, Tom ;

Pous, Damien .

SCIENTIFIC ANNALS OF COMPUTER SCIENCE, 2012, 22 (01) :147-199

[8]

Hyland JME, 2000, INFORM COMPUT, V163, P285, DOI 10.1006/inco2000.2917

[9] Full abstraction for functional languages with control [J].

Laird, J .

12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, :58-67

[10]

Laird James, 2001, Electronic Notes in Theoretical Computer Science, V45, P232, DOI [10.1016/S1571-0661(04)80965-4, DOI 10.1016/S1571-0661(04)80965-4]

← 1 2 →