A Categorical Model of an $$\mathbf {i/o}$$ -typed $$\pi $$ -calculus
A Categorical Model of an $$\mathbf {i/o}$$ -typed $$\pi $$ -calculus
复制标题
$$mathbf {i/o}$$ 型 $$pi $$ 微积分的分类模型
DOI：
10.1007/978-3-030-17184-1_23
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Tsukada Takeshi
中科院分区：
文献类型：
--
作者：
Sakayori Ken;Tsukada Takeshi
本文介绍了一种新的范畴结构，它是类型演算的一个变体的模型，就像一个范畴闭范畴是类型演算的一个模型一样。据我们所知，没有范畴模型已被给予的类型演算，相反，会话类型演算，相应的逻辑和范畴结构。本文引入的范畴结构具有简单的定义，它结合了两种著名的结构，即闭Freyd范畴和紧闭范畴。前者是在一般情况下有效计算的模型，后者描述了通过通道的连接，这导致了我们在本文中关注的效果。为了证明分类模型的相关性，我们通过语义考虑表明，演算等价于并发ML的核心演算。
This paper introduces a new categorical structure that is a model of a variant of the-typed-calculus, in the same way that a cartesian closed category is a model of the-calculus. To the best of our knowledge, no categorical model has been given for the-typed-calculus, in contrast to session-typed calculi, to which corresponding logic and categorical structure were given. The categorical structure introduced in this paper has a simple definition, combining two well-known structures, namely, closed Freyd category and compact closed category. The former is a model of effectful computation in a general setting, and the latter describes connections via channels, which cause the effect we focus on in this paper. To demonstrate the relevance of the categorical model, we show by a semantic consideration that the-calculus is equivalent to a core calculus of Concurrent ML.