消息传递的逻辑
The logic of message passing
摘要:
消息传递是并发编程的关键组成部分。本文的目的是描述消息传递的证明论、范畴语义学和术语演算之间的等价性。为了实现这一点,我们引入了线性范畴的范畴概念和相关的多元范畴概念。毫不奇怪,术语演算的符号大量借用了(同步)π演算。系统的切割消除过程提供了操作语义。
英文摘要:
Message passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message passing. In order to achieve this we introduce the categorical notion of a linear actegory and the related polycategorical notion of a poly-actegory. Not surprisingly the notation used for the term calculus borrows heavily from the (synchronous) pi-calculus. The cut elimination procedure for the system provides an operational semantics.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。