Two sides of the same coin: Session Types and Game Semantics
Two sides of the same coin: Session Types and Game Semantics
复制标题
同一枚硬币的两面：会话类型和游戏语义
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
N. Yoshida
中科院分区：
文献类型：
--
作者：
Simon Castelan;N. Yoshida
游戏语义和会话类型是相同概念的两个形式化：遵循某些协议的开放程序代表游戏作为策略，而会话类型指定协议；在本文中，给出了π级别的忠实模型，并确切地描述了策略。可以通过建立会话π -calculus的准确游戏语义模型来同时解决问题。为同步的同步计算开发基于事件的游戏语义进一步加强这种对应关系，通过内部会话π-钙化来建立异步策略的有限定义，作为这些结果的应用，我们提出了将同步策略忠实地编码在呼叫返回协议中的同步策略流程级别。策略和策略作为会话计算的非常准确的模型。
Game semantics and session types are two formalisations of the same concept: message-passing open programs following certain protocols . Game semantics represents protocols as games , and programs as strategies ; while session types specify protocols, and well-typed π -calculus processes model programs. Giving faithful models of the π -calculus and giving a precise description of strategies as a programming language are two difficult problems. In this paper, we show how these two problems can be tackled at the same time by building an accurate game semantics model of the session π -calculus. Our main contribution is to fill a semantic gap between the synchrony of the (session) π -calculus and the asynchrony of game semantics, by developing an event-structure based game semantics for synchronous concurrent computation. This model supports the first truly concurrent fully abstract (for barbed congruence) interpretation of the synchronous (session) π -calculus. We further strengthen this correspondence, establishing finite definability of asynchronous strategies by the internal session π -calculus. As an application of these results, we propose a faithful encoding of synchronous strategies into asynchronous strategies by call-return protocols, which induces automatically an encoding at the level of processes. Our results bring session types and game semantics into the same picture, proposing the session calculus as a programming language for strategies, and strategies as a very accurate model of the session calculus. We implement a prototype which computes the interpretation of session processes as synchronous strategies.