Session Types = Intersection Types + Union Types
Session Types = Intersection Types + Union Types
复制标题
会话类型 = 交集类型 联合类型
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
L. Padovani
中科院分区：
文献类型：
--
作者：
L. Padovani
我们提出了一种依赖交集和工会类型的会话类型的语义基础理论。我们认为，交集和联合类型是在会话类型中建模分支点的自然候选者，我们表明所产生的理论克服了相关行为理论的一些重要缺陷。特别是，交叉点和工会为计算加入和会议类型的会议的问题提供了本机解决方案。同样，子类型的关系事实证明是一个综合性，而相关行为理论并不总是如此。
We propose a semantically grounded theory of session types which relies on intersection and union types. We argue that intersection and union types are natural candidates for modeling branching points in session types and we show that the resulting theory overcomes some important defects of related behavioral theories. In particular, intersections and unions provide a native solution to the problem of computing joins and meets of session types. Also, the subtyping relation turns out to be a pre-congruence, while this is not always the case in related behavioral theories.