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.
Original language | English |
---|---|
Pages (from-to) | 498-533 |
Number of pages | 36 |
Journal | Science of Computer Programming |
Volume | 74 |
Issue number | 8 |
DOIs | |
Publication status | Published - 2009 |
Keywords
- Concurrency
- Linear actegory
- Linear distributive category
- Linear logic
- Message passing
- Multicategory
- Poly-actegory
- Polycategory
- Process semantics
- Term logic