The logic of message-passing

J.R. B. Cockett, Craig Antonio Pastro

    Research output: Contribution to journalArticlepeer-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 languageEnglish
    Pages (from-to)498-533
    Number of pages36
    JournalScience of Computer Programming
    Volume74
    Issue number8
    DOIs
    Publication statusPublished - 2009

    Keywords

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

    Fingerprint

    Dive into the research topics of 'The logic of message-passing'. Together they form a unique fingerprint.

    Cite this