Denotational reasoning for asynchronous multiparty session types

Reference: McDermott, D. & Yoshida, N. (2026). Denotational reasoning for asynchronous multiparty session types. 35th European Symposium on Programming (ESOP 2026), Turin, Italy. University of Oxford. PDF (Oxford MRG)

Summary

McDermott and Yoshida provide the first denotational semantics for asynchronous multiparty session types (MPST) with precise asynchronous subtyping. Where MPST has accumulated a vast operational and type-theoretic literature, no extensional denotational semantics for an expressive MPST calculus previously existed (binary session types had been given logical-relations and game-semantics models, but multiparty had not). The paper closes that gap with a model designed for reasoning: it is extensional, hiding non-observable behaviour (internal reductions) while capturing observable behaviour (sending a message), so that one can prove equivalences between syntactically distinct message-passing programs and justify communication optimisations — in particular those that reorder messages as permitted under asynchrony.

The central insight is that sending and receiving messages are computational effects, analogous to mutating state or raising an exception. The authors therefore design SafeMP, an idealised call-by-value language built on the fine-grain call-by-value calculus with asynchronous message-passing added as an effect plus first-order guarded recursive functions. Rather than the linear-logic foundation of most prior session-type systems, SafeMP is a graded type system: each computation carries both a type and a grade, and here the grades are multiparty session types, which carry exactly the information needed to enforce safety and liveness. This recasts “multiparty session typing is an instance of grading.” Because graded type systems are standardly modelled by graded monads, the paper introduces computation trees — a simple representation of asynchronous message-passing computation that accounts for asynchrony without explicit queues — and shows they form a graded monad. Computation trees yield an adequate denotational semantics for SafeMP with respect to a typed notion of bisimilarity that accounts for asynchrony, and the model is then used to prove communication safety, deadlock-freedom, and liveness even in the presence of communication optimisations.

A further contribution is a ground-up reformulation of asynchronous multiparty session subtyping. Taking the sound-and-complete (precise) asynchronous subtyping of Ghilezan et al. as its target, the paper gives the first definition that is sound and complete while (1) operating directly on session types rather than their infinite unfoldings as session trees, and (2) supporting subtyping for session types with free type variables (needed by SafeMP). For closed session types the new definition is shown equivalent to Ghilezan et al.

Key Ideas

First denotational semantics for asynchronous MPST with precise asynchronous subtyping; extensional, so it abstracts internal reductions while retaining observable message-passing — purpose-built for proving program equivalences and optimisation correctness.
Message-passing as a computational effect. Sending/receiving are treated like state or exceptions; the connection to the computational-effects literature is exploited throughout.
Grading instead of linearity. SafeMP is the first session type system for a call-by-value language based on grading (an effect system) rather than linear logic; the grades are multiparty session types. Multiparty session typing is exhibited as an instance of grading.
Computation trees as a graded monad. A simple representation of asynchronous computation that captures asynchrony without queues and forms the graded monad modelling SafeMP.
Adequacy w.r.t. asynchronous bisimilarity. Computation trees give an adequate denotational semantics for SafeMP relative to a typed bisimilarity that accounts for asynchrony, enabling reasoning about equivalences that rely on asynchrony (e.g. message reordering).
Reformulated asynchronous subtyping. First sound-and-complete asynchronous session subtyping that (a) avoids infinite session trees and (b) permits free type variables; equivalent to Ghilezan et al.’s precise subtyping on closed types.
Provable communication optimisations. Asynchrony admits more permissive subtyping (some synchronous deadlocks vanish), licensing practically useful optimisations; the model proves their correctness while preserving communication safety, deadlock-freedom, and liveness.
SafeMP operational vs denotational asymmetry. The operational semantics buffers messages into queues in the usual way; the denotational semantics achieves the same asynchrony with a simpler, queue-free setup.

Connections

Conceptual Contribution

Claim: Asynchronous multiparty session typing is an instance of grading, and asynchronous message-passing admits a simple, extensional denotational model — the first for MPST with precise asynchronous subtyping — that is adequate w.r.t. an asynchrony-aware bisimilarity and strong enough to prove the correctness of communication optimisations (message reordering) while guaranteeing communication safety, deadlock-freedom, and liveness.
Mechanism: Treat send/receive as computational effects; build SafeMP as a graded (effect) type system over fine-grain call-by-value with first-order guarded recursion, where the grades are multiparty session types; introduce computation trees as a queue-free representation of asynchronous computation forming a graded monad; interpret SafeMP into this monad and prove adequacy against a typed, asynchrony-accounting bisimilarity; reformulate asynchronous subtyping directly on session types (no session trees, free type variables allowed), shown equivalent to Ghilezan et al. on closed types.
Concepts introduced/used: computation trees, Graded Monad, Graded Type System, multiparty session types, Asynchronous Subtyping, Denotational Semantics, Computational Effects, SafeMP, fine-grain call-by-value, adequacy, asynchronous bisimilarity.
Stance: foundational / formal-semantic.
Relates to: Direct semantic complement to Multiparty Asynchronous Session Types (Honda, Yoshida & Carbone POPL 2008), which established the operational global-types → local-types → processes pipeline; this paper supplies the missing denotational account for the asynchronous multiparty setting and re-derives its subtyping. By founding session typing on grading rather than linear logic, it deliberately breaks with the Curry-Howard/linear-logic lineage that underlies most session-type systems, importing instead the graded-monad machinery from the computational-effects literature. Sits alongside On the Monitorability of Session Types as another semantic-foundations treatment of session types, and shares the Yoshida choreographic-programming family (Structured Communication-Centred Programming for Web Services) whose protocols project to the per-role session types this model interprets. The reordering-optimisation results connect to the broader asynchronous-subtyping program implemented in Rust, MPI and C and mechanised in Rocq.

Tags

#session-types #multiparty #denotational-semantics #asynchronous-subtyping #graded-monad #computational-effects #type-theory #foundational #yoshida

Backlinks

Linked Pages

Structured Communication-Centred Programming for Web Services

Reference: Carbone, M., Honda, K. & Yoshida, N. (2007/2012). Conference: European Symposium on Programming (ESOP 2007), LNCS 4421: 2–17. Journal: ACM Transactions on Programming Languages and Systems 34(2): 8:1–8:78, June 2012. DOI: 10.1145/2220365.2220367. Source file: carbone-honda-yoshida-toplas12.pdf. URL

Summary

Carbone, Honda and Yoshida introduce the formal foundation of what is now called Choreographic Programming: a programming paradigm in which one writes a global description of how a set of communicating agents interact — who sends what to whom, in what order, under which choices — and a mechanical endpoint projection derives the local program for each participant. The paper presents two formal calculi side by side: a global calculus whose terms describe interaction patterns from an Olympian, single-program perspective (e.g. A → B : op⟨v⟩.G, “A sends op carrying v to B, then continue with G”), and an end-point calculus — a session-typed asynchronous π-calculus — that describes the same interactions from each participant’s local perspective. The bridge between them is a projection function that, given a well-formed global description, produces a tuple of end-point processes, one per participant. The central technical result is a soundness and completeness correspondence (the Theorem of End-Point Projection): the global calculus and the projected end-point system are bisimilar, and the projection produces deadlock-free, communication-safe processes whenever the source global description satisfies a small set of well-formedness conditions (notably connectedness — every participant of a continuation must have been informed of the choice — and thread linearity).

The paper’s intellectual move is to elevate the interaction itself to the status of programmable artefact, replacing the dominant view in which communication patterns are inferred post hoc from local code. The motivation is the W3C Web Services Choreography Description Language (WS-CDL), but the calculus is independent of that context and has since become the foundation of an entire research line: subsequent work generalises the binary session-type substrate to multiparty (Multiparty Asynchronous Session Types, Honda-Yoshida-Carbone POPL 2008), embeds choreographies in production languages (Choral, HasChor, ChoRus), and extends the framework toward adversarial settings via cryptographic primitives. Every contemporary choreographic-programming paper — including Pact — descends from this work.

Key Ideas

Global calculus: a process calculus whose terms describe interactions from a vantage point above all participants. Primitives include sending (A → B : op⟨v⟩.G), branching (A → B : {labelᵢ : Gᵢ}), parallel composition, recursion, and assignment.
End-point calculus: an asynchronous, session-typed π-calculus describing each participant’s local view; communication occurs over named sessions with structured types.
Endpoint projection (EPP): a syntactic transformation ⟦G⟧_A mapping a global description G and a participant A to an end-point process. Type-driven and compositional.
Theorem of End-Point Projection: for every well-formed global description G, the parallel composition of its end-point projections is operationally equivalent (bisimilar) to G itself, and is deadlock-free and communication-safe.
Connectedness condition: a syntactic well-formedness check ensuring every participant in a continuation has been informed of the branch taken — this is what rules out projections in which one participant chooses a branch the others cannot observe.
Thread linearity: each session channel is owned by exactly one thread, making projection unambiguous.
Session types as the substrate: the global calculus is typed by global types, projected to local types per participant; well-typedness of the source guarantees well-typedness of all projections.
Operational correspondence at the core: global reductions are matched step-for-step by end-point system reductions, and vice versa, modulo τ-transitions for internal sequencing.

Connections

Conceptual Contribution

Claim: Distributed communication should be programmed globally — as a single artefact describing the joint interaction of all participants — rather than locally as per-process send/receive code, because the global view exposes the protocol’s structure to type-checking and admits a sound-and-complete mechanical projection to per-role implementations that are deadlock-free and communication-safe by construction.
Mechanism: Two parallel calculi (a global calculus describing interactions and an end-point asynchronous π-calculus describing local processes); a session-type discipline at both levels with a projection theorem showing global types project to local types role-by-role; a syntactic endpoint projection function ⟦G⟧_A mapping global descriptions to local processes; well-formedness conditions (connectedness, thread linearity) sufficient to guarantee that projection preserves operational behaviour and yields communication safety; the central Theorem of End-Point Projection establishing bisimulation between the global system and its projected end-point composition.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, Session Types, global type, local type, π-calculus, well-formedness (connectedness, thread linearity)
Stance: foundational / formal-semantic
Relates to: The taproot of the choreographic-programming literature. Sister paper to Multiparty Asynchronous Session Types (Honda-Yoshida-Carbone POPL 2008), which generalises the binary session-type substrate here to N-party interactions; together the two papers establish the modern global-types / local-types / endpoint-projection triangle. Underwrites the contemporary canonical reference Introduction to Choreographies (Montesi 2023). The runtime-monitoring story for the projected end-points is given by On the Monitorability of Session Types (Bartolo Burlò et al. ECOOP 2021). Structurally the exact analogue of Commitment Machines - Yolum and Singh (Yolum-Singh ATAL-01) and Flexible Protocol Specification and Execution (Yolum-Singh AAMAS-02) in the agent-communication tradition: both pairs (Carbone-Honda-Yoshida ↔ Yolum-Singh) take a globally-specified protocol, define a mechanical projection to per-role behaviour, and prove the projection preserves the relevant correctness property — communication safety on the choreography side, commitment discharge on the commitment-protocol side. Direct ancestor of Pact - A Choreographic Language for Agentic Ecosystems (Gopinathan et al. CP 2026), which adds game-theoretic operators on top of this substrate. The π-calculus dependency goes back to Communicating Sequential Processes (Hoare 1978) for the synchronous-communication root.

Tags

On the Monitorability of Session Types

On the Monitorability of Session Types, in Theory and Practice

Reference: Bartolo Burlò, C., Francalanza, A. & Scalas, A. (2021). 35th European Conference on Object-Oriented Programming (ECOOP 2021), LIPIcs vol. 194: 20:1–20:30. DOI: 10.4230/LIPIcs.ECOOP.2021.20. Extended version: arXiv:2105.06291. Source file: bartolo-burlo-francalanza-scalas-ecoop21.pdf. URL

Summary

Bartolo Burlò, Francalanza and Scalas address the monitorability problem for Session Types — the question of whether a runtime monitor, observing only the messages a process exchanges, can faithfully detect violations of a session-type specification. Session types are the dominant PL formalism for typing communicating processes (Honda, Vasconcelos, Yoshida), and they admit static type-checking when source is available; the runtime question matters because in many practical settings (third-party code, foreign-language components, dynamic deployments) only message traces are observable. The authors formalise session-monitored processes — a process algebra in which a monitor sits on the wire and interrupts ill-typed exchanges — and prove the central correctness pair: soundness (a monitor flags only processes that are actually ill-typed) and completeness (a monitor flags every ill-typed process whose violation is detectable from its observable trace).

The theoretical core is a precise characterisation of which session-type properties are monitorable from observable traces alone — distinguishing what static type-checking can decide (everything in the type) from what a dynamic monitor can decide (a strictly smaller class, characterised by the paper). On the practical side, the authors build a Scala toolkit that automatically generates session-type monitors from session-type specifications; the generated monitors instrument black-box processes written in any language, and the paper benchmarks the runtime overhead. The result is a working bridge from the theory of session types to deployable runtime conformance checking — and, by structural analogy, an off-the-shelf playbook for the same operation on commitment-based and choreographic protocols.

Key Ideas

Session-monitored processes: a process algebra extended with explicit monitors that observe message exchanges and rule them in or out against a session type.
Soundness of monitoring: a monitor never flags a well-typed process as a violator. (Verbatim: “monitors only flag ill-typed processes”.)
Completeness of monitoring: a monitor flags every ill-typed process whose violation is observable from the message trace.
Monitorability gap: not every session-type property is monitorable from observable traces — the paper characterises exactly which ones are.
Connection to static type-checking: the monitorable fragment is a strict sub-class of the statically-decidable fragment, and the paper precisely locates the gap.
Scala monitor toolkit: automatic generation of executable monitors from session-type specifications; works on black-box processes.
Empirical evaluation: benchmarks of monitor overhead on representative communication-heavy workloads.

Connections

Conceptual Contribution

Claim: Session types — like commitment-based protocols — admit a precise monitoring theory in which a runtime monitor observing only the message trace can be proved sound and complete with respect to a session-type specification, modulo a precisely-characterised gap between what is statically decidable and what is observable from traces alone; this theory can be discharged into an automatic toolkit that generates working monitors from specifications.
Mechanism: Define session-monitored processes as a process algebra with explicit on-wire monitors; formalise soundness (monitor flags only ill-typed processes) and completeness (every observable violation is flagged); characterise the monitorable fragment of session-type properties; implement an automatic monitor generator in Scala and benchmark its overhead on instrumented black-box processes.
Concepts introduced/used: Session Types, Runtime Verification, Monitorability, soundness, completeness, process algebra, Choreographic Programming, Endpoint Projection, Conversation Protocols
Stance: formal-semantic + engineering
Relates to: Structural sibling of the commitment-machine / commitment-protocol tradition: session types and commitment-based protocols are independently-developed formalisms for the same thing — typing communicating processes against a publicly-observable global protocol — and the runtime-monitoring theory developed here lifts almost directly to the commitment-machine setting (where Yolum-Singh’s “complete iff every base-level commitment is discharged” is the commitment-protocol analogue of session-type monitorability). Provides the theoretical engine for a runtime-conformance layer over choreographic protocols — choreographies project to per-role session types, which can then be monitored using this paper’s machinery, closing the gap that the Pact review opened (Pact has design-time game-theoretic analysis but no runtime conformance check). For CBCL - Safe Self-Extending Agent Communication, the paper supplies an analogue for the in-flight version of R5: where R5 checks contract well-formedness at install time, monitorability theory is the runtime story for the per-message-trace check. Companion to Verifiable Semantics for ACLs (Wooldridge 1998) in the unverifiability-becomes-decidability line: Wooldridge showed that mentalistic ACL semantics is undecidable; this paper shows that public, trace-based semantics admits sound-and-complete monitoring.

Tags

Graded Monad

(page does not exist)

Linear Logic

Girard’s resource-aware refinement of classical/intuitionistic logic (1987): the structural rules of weakening and contraction are removed and reintroduced under exponential modalities ! / ?. Connectives split into multiplicatives (⊗, ⅋) and additives (&, ⊕). The Curry–Howard counterpart of Session Types for the Pi-Calculus (Caires–Pfenning 2010, Wadler 2012): well-typed processes are deadlock-free and session-faithful, with cut elimination ⇔ communication.

In this vault

Multiparty Asynchronous Session Types

Reference: Honda, K., Yoshida, N. & Carbone, M. (2008). Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08), San Francisco, CA, pp. 273–284. ACM. DOI: 10.1145/1328438.1328472. Journal version: Journal of the ACM 63(1):9, 2016, DOI: 10.1145/2827695. Source file: honda-yoshida-carbone-popl08.pdf. URL

Summary

Honda, Yoshida and Carbone generalise the binary session-type discipline of Honda (1993) and Honda-Vasconcelos-Kubo (1998) to multiparty asynchronous communication: a single global type describes the interaction protocol among N ≥ 2 participants, and per-participant local types are derived by a syntactic projection function that translates each global statement into the participant’s local view of it. A process calculus extending the asynchronous π-calculus is typed against these local types; the central technical result is the subject reduction and progress theorem: a system of well-typed processes is deadlock-free, communication-safe (no message-type mismatch), and session-fidelity-preserving (the runtime trace conforms to the global type, projected). This three-tier structure — global types, local types via projection, processes typed against local types — is the formal foundation that the entire contemporary multiparty session-types and choreographic-programming literature inherits.

The paper’s intellectual contribution is to make the global protocol a typed object whose well-formedness can be checked once, with the well-typedness of every projected role following automatically. Where binary session types describe the obligations of two endpoints separately and rely on duality, multiparty session types describe the joint protocol once and project to as many roles as needed, with a coherence condition (each branching point is observed by every relevant participant) ensuring projections are mutually consistent. The treatment is asynchronous: send is non-blocking, messages are buffered in per-channel queues, and the type system tracks the resulting message-order obligations. The framework is the direct precursor of contemporary choreographic-programming languages (Choral, HasChor, ChoRus, Pact) and of the runtime-monitoring theory developed in On the Monitorability of Session Types.

Key Ideas

Global type: a single typing artefact G describing the interaction among N participants — primitives include p → q : ⟨S⟩.G (participant p sends a value of type S to q, then G), branching p → q : {ℓᵢ : Gᵢ}, recursion μt.G, and parallel composition.
Local type / projection: G ↾ p is the projection of G to participant p, syntactically translating each global statement into the corresponding send/receive/select/branch from p’s perspective.
Coherence (well-formedness): a global type is well-formed iff every choice point is observed by every relevant participant — the multiparty analogue of the connectedness condition in Structured Communication-Centred Programming for Web Services.
Asynchronous π-calculus substrate: processes communicate over typed session channels with non-blocking send and FIFO queues; each session is opened with a fresh name and closed structurally.
Subject reduction: well-typedness is preserved under reduction.
Communication safety: no well-typed system ever sends a value whose type the receiver does not expect.
Session fidelity / progress: the runtime trace of a well-typed system is a refinement of the projected local types, and well-typed systems whose buffers are empty cannot deadlock.
Type-driven engineering payoff: type-check the global protocol once, get communication-safety guarantees for every role for free.

Connections

Conceptual Contribution

Claim: Multiparty distributed communication is best disciplined by a single global type describing the joint protocol of all participants, from which per-participant local types are derived by mechanical projection; well-typedness of the global type plus a coherence condition ensuring choice points are observed by all relevant parties is sufficient to guarantee that every projected process is communication-safe, deadlock-free, and faithful to the global protocol.
Mechanism: Define global types as a calculus over N ≥ 2 participants with sending, branching, recursion, parallel composition; define local types as session types with send/receive/select/branch; define a syntactic projection G ↾ p from global to local types per participant; type processes (extended asynchronous π-calculus with FIFO message buffers) against the projected local types; prove subject reduction (well-typedness preserved under reduction), communication safety (no type-mismatched messages), and progress (well-typed systems with empty buffers do not deadlock).
Concepts introduced/used: Session Types, multiparty session types, global type, local type, projection, coherence, subject reduction, asynchronous π-calculus, communication safety, session fidelity
Stance: foundational / formal-semantic
Relates to: Companion to Structured Communication-Centred Programming for Web Services (Carbone-Honda-Yoshida ESOP 2007 / TOPLAS 2012) — the two papers together establish the modern global types → local types → processes pipeline that all subsequent choreographic-programming and multiparty session-types work inherits. Without the multiparty extension here, the binary session-type substrate of Carbone-Honda-Yoshida 2007 cannot scale to the N-participant choreographies that real protocols need. Underwrites the contemporary textbook Introduction to Choreographies (Montesi 2023). Provides the type-system substrate that On the Monitorability of Session Types (Bartolo Burlò et al. ECOOP 2021) lifts into a runtime-monitoring theory, and that Pact - A Choreographic Language for Agentic Ecosystems adds game-theoretic operators on top of. The structural counterpart in the agent-communication tradition is Commitment Machines - Yolum and Singh / Flexible Protocol Specification and Execution: both lineages (multiparty session types ↔ Yolum-Singh commitment protocols) take a globally-specified N-participant protocol, project to per-role views, and prove the projection preserves a key correctness property (communication safety here, commitment discharge there). The π-calculus substrate descends from Communicating Sequential Processes (Hoare 1978) and Milner’s π-calculus.

Tags

Computational Effects

(page does not exist)

Denotational Semantics

Scott-Strachey style: assign to each syntactic construct a mathematical denotation (function or domain element). Contrasts with operational and axiomatic semantics.

In this vault

Asynchronous Subtyping

(page does not exist)

Graded Type System

(page does not exist)

Pi-Calculus

A process calculus introduced by Milner, Parrow & Walker (1992) in which the names communicated between processes are themselves channels. Combines the parallel-composition and synchronisation primitives of CCS with name-passing, giving a single primitive that subsumes communication and dynamic network reconfiguration. The standard substrate for Session Types, Choreographic Programming, and modern formal accounts of Mobility and Concurrency. Comes in monadic, polyadic, asynchronous, higher-order, and applied (with cryptography) variants.

In this vault

A Calculus of Mobile Processes — Milner, Parrow & Walker 1992 (original)
A Calculus of Communicating Systems — Milner 1980 (predecessor)
Communicating Sequential Processes — Hoare 1978 (sibling)
Mobile Ambients — Cardelli & Gordon 1998 (locations-first sibling)
Spi Calculus — Abadi & Gordon 1997 (cryptographic extension)
Join Calculus — Fournet & Gonthier 1996 (asynchronous reformulation)
Sjoin Calculus
Session Types
Multiparty Asynchronous Session Types
Structured Communication-Centred Programming for Web Services
Choreographic Programming
Pact - A Choreographic Language for Agentic Ecosystems
Name-Passing
Scope Extrusion
Bisimulation
Mobility
Process Calculi

Endpoint Projection

The mechanical translation from a global choreographic program — which describes the joint behaviour of all participants — to a per-participant local program that, when run in parallel with the others, realises the choreography. Endpoint projection is the operation that makes Choreographic Programming practical: the global program is the source of truth, and projection to each role is a syntactic/semantic transformation that preserves the communication structure and (under standard well-formedness conditions) deadlock-freedom. Implementations differ in how role information is tracked — type-system roles (Choral, ChoRus), census polymorphism (Bates et al. 2025), or algebraic-effect handlers (Pact, Effectful) — but all share the global-to-local move that distinguishes choreographic from session-typed programming. The structural analogue in commitment-based protocol theory is Commitment Machines, which compiles a global commitment specification to per-role finite-state machines.

In this vault

Choreographic Programming
Structured Communication-Centred Programming for Web Services — origin of the Theorem of End-Point Projection
Multiparty Asynchronous Session Types — multiparty projection G ↾ p
Introduction to Choreographies
Session Types
Pact - A Choreographic Language for Agentic Ecosystems
Commitment Machines
Algebraic Effects

Bisimulation

A coinductive equivalence on labelled transition systems: two states are bisimilar iff every transition from one can be matched by a transition with the same label from the other, and the resulting states remain bisimilar. The standard behavioural equivalence for process calculi (CCS, Pi-Calculus, CSP). Strong bisimulation matches every transition including silent ones; weak bisimulation absorbs internal τ-transitions. In Pi-Calculus three sub-variants — early, late, and open — differ in when an input action’s bound name is instantiated, with open bisimulation alone preserved by all contexts.

In this vault

Call-by-Value

(page does not exist)

Liveness Property

A property of a program or distributed system asserting that “something good eventually happens” (Lamport 1977; Alpern & Schneider 1985). Unlike a Safety Property, a liveness property cannot be falsified by any finite prefix — one must observe (or reason about) infinite behaviours.

Examples: eventual delivery (“every sent message is eventually received”), progress (“every enabled thread eventually runs”), termination (“every well-formed input produces output”). Proving liveness typically requires a well-founded ordering or a fairness assumption.

Alpern–Schneider’s decomposition theorem: every trace property is the intersection of a safety property and a liveness property. This factoring structures verification: safety is proved by invariants, liveness by well-founded descent or fairness-conditioned reasoning.

Tags

#verification #distributed-systems #safety-liveness

Deadlock Freedom

(page does not exist)

Communication Safety

(page does not exist)

Session Types

A type discipline for communicating processes — originating with Honda (1993) and developed extensively by Honda, Vasconcelos, Yoshida, and others — in which a process’s communication behaviour is typed by a session type: a structured description of the sequence of messages that may flow on a channel, including alternation (!/?), choice (+/&), recursion, and delegation. Session types come in two flavours: binary (two participants per channel) and multiparty (a global type projected to per-role local types — directly analogous to choreographic Endpoint Projection). When a process can be source-checked, its session-type conformance is decidable statically; when it cannot, runtime monitors can enforce the type from observable message traces (On the Monitorability of Session Types). Structurally adjacent to the commitment-based protocol tradition: session types and Yolum-Singh-style commitment protocols are independently-developed formalisms for typing communicating agents against a publicly-observable global protocol.

In this vault

Multiparty Asynchronous Session Types — Honda, Yoshida & Carbone POPL 2008, the multiparty session-types foundation
Structured Communication-Centred Programming for Web Services — Carbone, Honda & Yoshida 2007/2012, choreographies built on session types
Introduction to Choreographies
On the Monitorability of Session Types
Choreographic Programming
Endpoint Projection
Commitment Machines - Yolum and Singh
Flexible Protocol Specification and Execution
Conversation Protocols
Pact - A Choreographic Language for Agentic Ecosystems