Label-dependent session types
Label-dependent session types
复制标题
标签相关的会话类型
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
V. Vasconcelos
中科院分区：
文献类型：
--
作者：
Peter Thiemann;V. Vasconcelos
会话类型已经作为通信协议的类型规则出现。具有会话类型的现有演算配备有许多不同的原语，这些原语将联合收割机通信与所传输值的引入或消除相结合。我们提出了一个基本的会话类型演算与轻量级的操作语义。它从数据的引入和消除完全简化了通信，因此具有单个通信减少的功能，它充当了接收器和接收器之间的会合。我们通过引入标签依赖的会话类型来实现这种解耦，这是一个具有子类型的最低限度的值依赖的会话类型系统。该系统是足够强大的模拟现有的功能会话类型的系统。与这样的系统相比，标签依赖的会话类型对代码的限制更少。我们进一步介绍原始递归自然数的类型级别，从而允许描述协议的行为取决于在消息中交换的数字。介绍了一个算法类型检查系统，并证明其与声明式系统是等效的。新的演算展示了依赖类型和线性类型的新型轻量级集成，其用途超出了会话类型系统。
Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the transmitted value. We present a foundational session type calculus with a lightweight operational semantics. It fully decouples communication from the introduction and elimination of data and thus features a single communication reduction, which acts as a rendezvous between senders and receivers. We achieve this decoupling by introducing label-dependent session types, a minimalist value-dependent session type system with subtyping. The system is sufficiently powerful to simulate existing functional session type systems. Compared to such systems, label-dependent session types place fewer restrictions on the code. We further introduce primitive recursion over natural numbers at the type level, thus allowing to describe protocols whose behaviour depends on numbers exchanged in messages. An algorithmic type checking system is introduced and proved equivalent to its declarative counterpart. The new calculus showcases a novel lightweight integration of dependent types and linear typing, with has uses beyond session type systems.
用于分布式面向对象编程的模块化会话类型
DOI：
10.1145/1706299.1706335
发表时间：
2010
期刊：
--
影响因子：
--
作者：
Gay S
通讯作者：
Gay S