Domain-Aware Session Types (Extended Version)

Bernardo Toninho; Frank Pfenning; Jorge A. P\'erez; Lu\'is Caires

arxiv: 1907.01318 · v1 · pith:JWU5NO3Vnew · submitted 2019-07-02 · 💻 cs.LO

Domain-Aware Session Types (Extended Version)

Lu\'is Caires , Jorge A. P\'erez , Frank Pfenning , Bernardo Toninho This is my paper

Pith reviewed 2026-05-25 10:35 UTC · model grok-4.3

classification 💻 cs.LO

keywords session typeslinear logichybrid logicdomain migrationaccessibility relationmultiparty protocolsprocess calculustype safety

0 comments

The pith

Extending linear logic with hybrid modal worlds produces domain-aware session types that enforce accessibility while preserving fidelity and progress.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a generalization of binary session types by extending linear logic with hybrid logic features, specifically modal worlds that represent domains and are governed by a parametric accessibility relation. This yields a typed process framework where well-typed processes are guaranteed to respect domain accessibility even when domain identities are known only at runtime. The same foundations support domain-aware multiparty session types whose global protocols can include arbitrarily nested sub-protocols through domain migration, with complex protocols reduced to the binary case for analysis. A sympathetic reader would care because the approach supplies logical guarantees for safe message-passing concurrency in settings with explicit domain constraints.

Core claim

By incorporating modal worlds and a parametric accessibility relation into linear logic, the resulting typed process calculus ensures that well-typed processes enjoy session fidelity, global progress, and termination, while communicating only with accessible domains; the framework further allows domain information to be supplied at runtime and supports the transfer of these properties to multiparty protocols via reduction to the binary setting.

What carries the argument

Hybrid-logic modal worlds indicating domains, governed by a parametric accessibility relation from Kripke semantics.

If this is right

Well-typed processes enjoy session fidelity, global progress, and termination.
Processes communicate only with domains that satisfy the accessibility relation.
Domain information determined only at runtime can still be statically enforced.
Domain-aware multiparty protocols with nested sub-protocols can be analyzed by reduction to the binary framework.
Correctness properties transfer from the binary to the multiparty setting.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same modal extension might apply to other concurrency calculi that currently lack location or domain constraints.
Runtime domain identities could be modeled as fresh constants without losing the static accessibility invariant.
Protocols involving dynamic network topologies become amenable to the same termination and progress arguments.
The reduction technique for multiparty protocols could generalize to other global-type extensions.

Load-bearing premise

The chosen extension of linear logic by hybrid-logic modal worlds and a parametric accessibility relation preserves the standard session-type guarantees while correctly enforcing domain migration even when domain identities are known only at runtime.

What would settle it

A concrete well-typed process that communicates with an inaccessible domain or violates global progress would falsify the central claim.

read the original abstract

We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that processes only communicate with accessible domains and so respect the accessibility relation. Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced. As a specific application, we introduce domain-aware multiparty session types, in which global protocols can express arbitrarily nested sub-protocols via domain migration. We develop a precise analysis of these multiparty protocols by reduction to our binary domain-aware framework: complex domain-aware protocols can be reasoned about at the right level of abstraction, ensuring also the principled transfer of key correctness properties from the binary to the multiparty setting.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This extends session types with hybrid worlds for domains and keeps the core guarantees, with the multiparty reduction as the practical payoff.

read the letter

This paper's main move is to add domain migration to the Curry-Howard reading of session types by layering hybrid modal worlds on linear logic, with a parametric accessibility relation controlling where processes can go. The result is a typed process calculus that statically enforces domain respect even when domain identities are discovered only at runtime. They then reduce domain-aware multiparty protocols to this binary setting so the same properties carry over. That reduction is the part that feels most immediately useful for protocol designers who already work with global types. The logical setup is the strength here: fidelity, progress, and termination follow from the typing rules in the usual way, and the accessibility checks are baked into the modal connectives rather than added as side conditions. The examples show how flexible relations can be defined and still checked, which is cleaner than most ad-hoc location annotations in the literature. The soft spots are limited. Leaving the accessibility relation parametric is the right design choice for generality, but it does mean that any concrete deployment still needs a separate argument that the chosen relation is the right one for the system; the paper does not supply tool support or decidability results for that step. The multiparty reduction is sketched at a high level, so a referee would want to see the full details of how the domain migration rules compose. Overall this is for people already inside session types and linear-logic concurrency who want a uniform account of location. It is worth sending to peer review because the core construction is non-routine and the properties are stated precisely enough to be checked.

Referee Report

0 major / 3 minor

Summary. The paper develops a generalization of Curry-Howard interpretations of binary session types by extending linear logic with hybrid logic modal worlds for domains, governed by a parametric accessibility relation. It claims that well-typed processes enjoy session fidelity, global progress, and termination while respecting the accessibility relation, including cases where domain identities are known only at runtime. The work further introduces domain-aware multiparty session types whose global protocols can express nested sub-protocols via domain migration, with a precise analysis obtained by reduction to the binary framework that transfers key correctness properties.

Significance. If the central claims hold, the work is significant for supplying logical foundations that statically enforce domain constraints and accessibility in message-passing concurrency while preserving standard session-type guarantees. The hybrid-logic extension cleanly handles runtime domain knowledge and flexible accessibility relations. The reduction-based treatment of multiparty protocols is a strength, as it enables reasoning at the appropriate level of abstraction and principled property transfer from the binary setting.

minor comments (3)

The abstract employs the subjective qualifier 'Remarkably'; a more neutral formulation would improve formality.
[§2] §2 (or the section introducing the hybrid-logic extension): an early concrete example of a parametric accessibility relation and its enforcement at runtime would aid readability.
Ensure that all references to prior work on hybrid logic, modal extensions of linear logic, and domain-specific concurrency are complete and up to date.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work, the accurate summary of its contributions, and the recommendation for minor revision. The referee's description correctly captures the logical foundations, the handling of runtime domain information, the preservation of session fidelity/progress/termination, and the reduction-based treatment of domain-aware multiparty protocols.

Circularity Check

0 steps flagged

No significant circularity in the logical extension

full rationale

The paper defines an extension of linear logic with hybrid-logic modal worlds and a parametric accessibility relation, then derives session fidelity, global progress, termination, and domain accessibility enforcement directly from the resulting typing rules and Curry-Howard interpretation. These properties are proven from the logical foundations rather than reducing by construction to any fitted parameters, self-defined quantities, or prior author-specific ansatzes. The reduction of multiparty protocols to the binary framework is a standard embedding analysis, not a statistical fit. Self-citations to prior session-type work are present but serve only as background; the central claims rest on the independent definitions and proof sketches given in the manuscript, which are self-contained against the external benchmarks of linear and modal logic.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The work rests on standard linear logic for session types and standard Kripke semantics for the accessibility relation; the modal worlds for domains are introduced as the central modeling device.

axioms (2)

standard math Linear logic provides the Curry-Howard foundation for binary session types
Invoked as the starting point for the generalization.
standard math Hybrid logic supplies modal worlds and a parametric accessibility relation with Kripke semantics
Used to model domains and migration constraints.

invented entities (1)

Domain-aware session types no independent evidence
purpose: Typed processes that respect domain accessibility while performing message-passing
New typed process framework introduced by the extension.

pith-pipeline@v0.9.0 · 5734 in / 1413 out tokens · 46196 ms · 2026-05-25T10:35:30.318586+00:00 · methodology

Domain-Aware Session Types (Extended Version)

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)