The analysis of communication network processes is an important topic in computer science. This paper compares two formalisms for describing such networks, namely linear logic (originally derived from an investigation into the fine structure of logical proofs) and session types (developed as a theoretical underpinning of the Scribble language). The paper’s main contribution is twofold:

(1) It shows (via a translation) that session types are strictly more expressive than session-based interpretations of linear logic.

(2) It shows that the rules of a linear logic can be extended by new typing rules without changing the term syntax, resulting in richer interconnection structures while keeping the desirable properties of typing.

The paper starts with the usual introduction and motivation, followed by an introduction to the two formal systems studied: linear logic in the context of session types, and the multiparty session calculus.

The next three sections form the core of the paper. Section 3 presents a translation from (a restricted version of) linear logic to session types. Next, section 4 investigates the composability of multiparty session types and derives a compatibility condition on session types that guarantees deadlock freedom. An important concept for this condition is so-called “partial global types,” and section 5 therefore investigates the partial global type generated by section 3’s translation.

The following two sections extend the previous sections by slowly lifting the restrictions used in these formalisms.

Section 8 introduces two multicut typing rules for linear logic (relying on the compatibility conditions developed in the previous sections). It presents an example of an interconnection that is not typeable with the usual typing rules, but is typeable with the multicut.

The paper closes with related work and some open questions for further research.

The paper is essentially self-contained, that is, it is readable without prior exposure to the formalisms discussed. Several well-chosen examples illustrate the technical definitions. Sometimes the intuition underlying a formalism is explained later on in the paper, so if something does not make sense at first, it might be useful to just continue reading and come back to it.