A Calculus of Global Interaction based on Session Types
A Calculus of Global Interaction based on Session Types
复制标题
DOI：
10.1016/j.entcs.2006.12.041
复制
发表时间：
2007-06-14
影响因子：
--
通讯作者：
Yoshida, Nobuko
中科院分区：
文献类型：
--
作者：
Carbone, Marco;Honda, Kohei;Yoshida, Nobuko
本文提出了一种用于描述以通信为中心的程序的微积分，并通过对实际业务协议中的几个用例的正式描述来讨论其使用。这种形式主义被称为全局演算，旨在将全球消息流表示为结构化通信。全局演算起源于编排描述语言（CDL），这是一种由 W3C 的 WS-CDL 工作组开发的 Web 服务描述语言。它的类型规则基于在 p-演算背景下经过多年研究的会话类型 [15,10,22,6]。会话类型为复杂的通信行为提供了高级抽象和表达，并在指导程序员对业务协议进行清晰、结构良好的描述方面发挥着基础作用。
This paper proposes a calculus for describing communication-centred programs and discusses its use through a formal description of several use cases from real business protocols. The formalism, called global calculus, aims at representing global message flows as structured communications. The global calculus originates from the Choreography Description Language (CDL), a web service description language developed by W3C's WS-CDL Working Group. Its type discipline is based on session types which have been studied over long years in the context of the p-calculus [15,10,22,6]. Session types offer a high-level abstraction and articulation for complex communication behaviours, and play a fundamental role to guide the programmer towards a clear, well-structured description of business protocols.