具有运行时适应性的会话类型:概述与示例
编程语言
2013-12-11 v1 计算机科学中的逻辑
摘要
在最近的工作中,我们为一种演算开发了一套会话类型规范,该演算不仅包含用于会话建立和通信的常规构造,还包含两个新颖的构造,使得通信进程能够在运行时被停止、复制或丢弃。旨在理解已知结构化通信静态分析技术是否能扩展到具有上下文感知和可适应性的分布式系统这一挑战性环境中,其中规范化的交互与运行时适应性是交织在一起的关注点。在本简短说明中,我们总结了具有运行时适应性的会话类型框架的主要特征,并回顾了其基本正确性属性。我们通过示例说明了我们的框架。特别是,我们展示了监督树的会话表示,这是一种在 Erlang 语言中强制执行容错应用的机制。
引用
@article{arxiv.1312.2699,
title = {Session Types with Runtime Adaptation: Overview and Examples},
author = {Cinzia Di Giusto and Jorge A. Pérez},
journal= {arXiv preprint arXiv:1312.2699},
year = {2013}
}
备注
In Proceedings PLACES 2013, arXiv:1312.2218