Nested Protocols in Session Types
Nested Protocols in Session Types
复制标题
会话类型中的嵌套协议
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Kohei Honda
中科院分区：
文献类型：
--
作者：
R. Demangeon;Kohei Honda
我们提出了一个改进的会话类型，引入嵌套协议，从父协议调用子协议的可能性。这个特性为现有的会话类型理论增加了表达性和模块性，允许传递参数并支持更高阶的协议定义。我们的理论是通过一个新的类型系统的协议处理子协议调用，其实现在会话演算。我们提出验证和满意度之间的关系规范和实现。良好的行为是强制执行感谢使用的种类和良好的形式，使我们能够确保进步和主题减少。此外，我们描述了我们的框架的扩展，允许子协议发回的结果。
We propose an improvement to session-types, introducing nested protocols, the possibility to call a subprotocol from a parent protocol. This feature adds expressiveness and modularity to the existing session-type theory, allowing arguments to be passed and enabling higher-order protocols definition. Our theory is introduced through a new type system for protocols handling subprotocol calls, and its implementation in a session-calculus. We propose validation and satisfaction relations between specification and implementation. Sound behaviour is enforced thanks to the usage of kinds and well-formedness, allowing us to ensure progress and subject reduction. In addition, we describe an extension of our framework allowing subprotocols to send back results.