Synchronous Game Semantics via Round Abstraction

被引:0
作者
Ghica, Dan R. [1 ]
Menaa, Mohamed N. [1 ]
机构
[1] Univ Birmingham, Birmingham B15 2TT, W Midlands, England
来源
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES | 2011年 / 6604卷
基金
英国工程与自然科学研究理事会;
关键词
SYNTACTIC CONTROL; FULL ABSTRACTION; INTERFERENCE; CONCURRENCY; MODEL; PCF;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
A synchronous game semantics-one in which several moves may occur simultaneously-is derived from a conventional (sequential) game semantics using a round abstraction algorithm. We choose the programming language Syntactic Control of Interference and McCusker's fully abstract relational model as a convenient starting point and derive a synchronous game model first by refining the relational semantics into a trace semantics, then applying a round abstraction to it. We show that the resulting model is sound but not fully abstract. This work is practically motivated by applications to hardware synthesis via game semantics.
引用
收藏
页码:350 / +
页数:2
相关论文
共 19 条
  • [1] Abramsky S, 2000, INFORM COMPUT, V163, P409, DOI [10.1006/inco.2000.2930, 10.1006/inco2000.2930]
  • [2] Reactive modules
    Alur, R
    Henzinger, TA
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 1999, 15 (01) : 7 - 48
  • [3] THE ESTEREL SYNCHRONOUS PROGRAMMING LANGUAGE - DESIGN, SEMANTICS, IMPLEMENTATION
    BERRY, G
    GONTHIER, G
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1992, 19 (02) : 87 - 152
  • [4] Cousot P., 1977, P ACM S PRINC PROGR, P238, DOI DOI 10.1145/512950.512973
  • [5] Ghica Dan R., 2007, POPL 2007. The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, P363, DOI 10.1145/1190216.1190269
  • [6] Ghica D.R., 2011, POPL IN PRESS
  • [7] Ghica D.R., 2010, MFPS 26, VXXVI
  • [8] Angelic semantics of fine-grained concurrency
    Ghica, Dan R.
    Murawski, Andrzej S.
    [J]. ANNALS OF PURE AND APPLIED LOGIC, 2008, 151 (2-3) : 89 - 114
  • [9] Ghica DR, 2010, LECT NOTES COMPUT SC, V6269, P417, DOI 10.1007/978-3-642-15375-4_29
  • [10] Ghica DR, 2006, LECT NOTES COMPUT SC, V3920, P303