Precise subtyping for synchronous multiparty sessions
Precise subtyping for synchronous multiparty sessions
复制标题
同步多方会话的精确子类型
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
N. Yoshida
中科院分区：
文献类型：
--
作者：
M. Dezani;S. Ghilezan;S. Jaksic;J. Pantović;N. Yoshida
亚型的概念在理论和应用领域都发挥了重要作用：在lambda和并发的骨化以及编程语言中。可以从两种不同的角度考虑，合理性和完整性共同称为亚型的准确性：操作和含义。最近已经开发了对类型安全性的精确性，即当期望较大类型的术语时，较小类型的术语的安全更换。后者的精确性基于一种类型的表示，该类型是一种数学对象，该对象根据语言的其他表达方式描述了类型的含义。本文的结果是同步多党会话的亚型的操作和指示性准确性。本文的新颖性是引入特征性的全球类型来证明运营完整性。
The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.