The logic of message-passing |
| |
| Authors: | JRB Cockett Craig Pastro |
| |
| Affiliation: | a Department of Computer Science, University of Calgary, 2500 University Drive NW, Calgary, Alberta T2N 1N4, Canada
b Department of Mathematics, Macquarie University, NSW 2109, Australia |
| |
| Abstract: | 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) π-calculus. The cut-elimination procedure for the system provides an operational semantics. |
| |
| Keywords: | Message passing Concurrency Process semantics Linear logic Term logic Multicategory Polycategory Linear distributive category Poly-actegory Linear actegory |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
