The logic of message-passing

J.R. B. Cockett; Craig Antonio Pastro

doi:10.1016/j.scico.2007.11.005

The logic of message-passing

J.R. B. Cockett, Craig Antonio Pastro

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

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	https://doi.org/10.1016/j.scico.2007.11.005
Publication status	Published - 2009

Keywords

Concurrency
Linear actegory
Linear distributive category
Linear logic
Message passing
Multicategory
Poly-actegory
Polycategory
Process semantics
Term logic

Access to Document

10.1016/j.scico.2007.11.005

Cite this

@article{fdc53c35ffe44c71894309e2045dc21c,

title = "The logic of message-passing",

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 = "Concurrency, Linear actegory, Linear distributive category, Linear logic, Message passing, Multicategory, Poly-actegory, Polycategory, Process semantics, Term logic",

author = "Cockett, {J.R. B.} and Pastro, {Craig Antonio}",

year = "2009",

doi = "10.1016/j.scico.2007.11.005",

language = "English",

volume = "74",

pages = "498--533",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

number = "8",

}

TY - JOUR

T1 - The logic of message-passing

AU - Cockett, J.R. B.

AU - Pastro, Craig Antonio

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - Concurrency

KW - Linear actegory

KW - Linear distributive category

KW - Linear logic

KW - Message passing

KW - Multicategory

KW - Poly-actegory

KW - Polycategory

KW - Process semantics

KW - Term logic

U2 - 10.1016/j.scico.2007.11.005

DO - 10.1016/j.scico.2007.11.005

M3 - Article

VL - 74

SP - 498

EP - 533

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

IS - 8

ER -

The logic of message-passing

Abstract

Keywords

Access to Document

Fingerprint

Cite this