Less is More: Multiparty Session Types Revisited

Reference: Scalas, A. & Yoshida, N. (2019). Less is More: Multiparty Session Types Revisited. Proceedings of the ACM on Programming Languages, 3(POPL), Article 30, pp. 1–29. ACM (POPL 2019). DOI: 10.1145/3290343. Artifact: mpstk, the Multiparty Session Types toolKit. Preprint (Imperial MRG) · Technical report DTRS18-6 · Artifact

Summary

Scalas and Yoshida revisit the foundations of multiparty session types (MPST) and argue that the classic theory of Honda–Yoshida–Carbone is built on machinery — a well-formed global type, mechanical projection to local types, and endpoint duality — that is both more restrictive and more fragile than it needs to be. They show that the classic global-types-plus-projection pipeline enjoys only a limited subject reduction property: its type-preservation and safety results hold only under side conditions that are easily overlooked, and several published MPST proofs were in fact flawed because those conditions silently failed. Their thesis is that these restrictions are an artefact of the presentation, not of the underlying discipline.

In place of the three-tier apparatus, the paper develops a generalised MPST theory grounded directly on behavioural properties of typing contexts. A typing context here is just a collection of local session types (one per role/channel); it has its own labelled transition system, and one can ask model-checking-style questions about it directly: is it safe (no role ever offers a message the others cannot receive), deadlock-free, live? The central move is to parameterise type soundness over an abstract safety predicate φ: the authors prove that whenever a typing context satisfies φ, the processes typed against it inherit the corresponding runtime guarantee (subject reduction, communication safety, and — for the stronger predicates — deadlock-freedom and liveness). Crucially, no global type and no duality relation are required: a projected global type becomes merely one convenient way to obtain a safe context, a special case the new theory subsumes rather than depends on. Because these behavioural properties are decidable on finite contexts, the authors implement mpstk, a toolkit that discharges safety, deadlock-freedom and liveness by translating typing contexts into the mCRL2 model checker — turning MPST verification into push-button checking and allowing them to certify correct systems that the classic theory rejects.

“Less is more” names the result: by removing global types and duality — the two heaviest ingredients of classic MPST — the theory becomes at once simpler (fewer definitions, fewer side conditions) and strictly more general (it types more well-behaved systems and repairs the soundness gaps of prior work).

Key Ideas

Behavioural typing contexts as first-class objects: a set of local session types is given an LTS of its own, and correctness is stated as properties of that LTS rather than as conformance to a global type.
Type safety parameterised by a property φ: a single meta-theorem shows that φ-safety of the context implies the matching runtime guarantee for typed processes; safety, deadlock-freedom and liveness are instances of increasing strength.
No global types required: global types are recast as an over-approximation — a sufficient (not necessary) recipe for producing a safe context — so classic MPST is a strict special case.
No duality required: binary endpoint duality, the correctness backbone of two-party session types, is dropped in favour of the behavioural predicates.
Repairs limited subject reduction: the classic projection-based theory only preserves typing under restrictive conditions; the generalised theory removes them and fixes flawed safety proofs in the literature.
Decidability and tooling: for finite typing contexts the properties are decidable; mpstk discharges them via the mCRL2 model checker, giving automated verification.
More typable systems: protocols that are safe but not the projection of any well-formed global type (or that violate the classic side conditions) are now typable and provably correct.

Connections

Conceptual Contribution

Claim: The correctness of multiparty session-typed systems does not require a global type, projection, or endpoint duality; it is fully captured by behavioural properties of the local typing context (safety, deadlock-freedom, liveness). Removing the classic machinery yields a theory that is simultaneously simpler and strictly more general, and repairs soundness flaws (the limited subject reduction of projection-based MPST) present in prior work.
Mechanism: Equip a typing context (a multiset of local session types) with a labelled transition system; define an abstract safety predicate φ over such contexts; prove a parameterised soundness theorem — φ-safety of the context implies subject reduction and the corresponding runtime guarantee for processes typed against it; instantiate φ as safety, deadlock-freedom and liveness. Recover classic MPST by exhibiting projected global types as one family of φ-safe contexts. Implement decision procedures for these properties in mpstk on top of the mCRL2 model checker.
Concepts introduced/used: behavioural typing, typing-context safety property (φ), deadlock-freedom, Liveness, subject reduction, generalised MPST without global types or Duality, model-checking-based verification (mpstk / mCRL2).
Stance: foundational / formal-semantic (with an implemented verification tool).
Relates to: A direct revision of Multiparty Asynchronous Session Types (Honda–Yoshida–Carbone POPL 2008), whose global type → projection → local type pipeline it generalises and whose subject-reduction limitations it diagnoses and fixes; the global-programming line of Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming (Carbone & Montesi) obtains deadlock-freedom by construction from a global program, whereas this paper obtains it by verification of a local context, making the two complementary routes to the same guarantee. Shares its verification-of-local-types outlook with On the Monitorability of Session Types (Bartolo Burlò, Francalanza & Scalas) — same second author lineage on the Scalas side — which synthesises runtime monitors rather than static model checks. Later denotational work Denotational Reasoning for Asynchronous Multiparty Session Types (McDermott & Yoshida) revisits asynchronous MPST from a semantic angle. The underlying process substrate is the asynchronous Pi-Calculus (Milner et al.), and the resource-sensitive reading of session types descends from Linear Logic via the Curry–Howard correspondence for sessions.

Tags

#session-types #multiparty #behavioural-types #deadlock-freedom #model-checking #pi-calculus #foundational #type-theory #mpstk

Backlinks

Linked Pages

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

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

Denotational Reasoning for Asynchronous Multiparty Session Types

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.

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

Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming

Deadlock-freedom-by-design: Multiparty Asynchronous Global Programming

Reference: Carbone, M. & Montesi, F. (2013). Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13), Rome, Italy. ACM. DOI: 10.1145/2480359.2429101. URL · PDF

Summary

Carbone and Montesi present a global programming (choreographic) language for asynchronous multiparty sessions whose defining property is that well-typed programs are deadlock-free by construction — even when they interleave several sessions at once. The starting observation is a gap in the multiparty session-types pipeline established by Multiparty Asynchronous Session Types: that discipline guarantees progress within a single session, but a participant engaged in multiple concurrent sessions can still deadlock, because cyclic wait-for dependencies can form across sessions (A waits on B in session s while B waits on A in session s′). Local, per-session typing cannot see those cross-session cycles. The paper’s move is to lift programming back to the global viewpoint of Structured Communication-Centred Programming for Web Services: one writes a single choreography describing who communicates with whom, in what order, across all the sessions involved, and a mechanical Endpoint Projection derives the local process for each role.

Because a choreography sequences interactions from an Olympian, single-program perspective, it cannot express a global cyclic wait — the global description is intrinsically free of the mismatched send/receive orderings that produce deadlock. The technical contribution is to carry that guarantee through projection: the authors define a choreography calculus over an asynchronous, session-typed process model (with message queues), give a typing discipline for choreographies that use and interleave multiple sessions, and prove an endpoint-projection theorem establishing operational correspondence between a choreography and the parallel composition of its projected endpoints. As a corollary, the distributed endpoint system inherits the choreography’s deadlock-freedom and communication safety — including across interleaved sessions — so deadlock-freedom is obtained by design rather than checked or repaired after the fact. The work is a direct precursor of the choreographic-programming languages that follow (Choral, HasChor, ChoRus) and is consolidated in Introduction to Choreographies.

Key Ideas

Global programming over multiparty sessions: programs are choreographies — global descriptions of the joint interaction of all participants — rather than per-role send/receive code, extending the global-calculus idea of Structured Communication-Centred Programming for Web Services to a full programming language.
Cross-session deadlock is the target: single-session progress (à la Multiparty Asynchronous Session Types) does not imply global deadlock-freedom once a participant interleaves multiple sessions; cyclic dependencies can span sessions where no single session’s type can detect them.
Deadlock-freedom by construction: a choreography cannot express a global cyclic wait, so well-typed global programs are deadlock-free by their very structure — the guarantee is intrinsic, not an external check.
Asynchronous session model: communication is non-blocking with message buffers/queues; the type discipline tracks the resulting ordering obligations across the interleaved sessions.
Endpoint Projection (EPP): a mechanical, type-driven transformation mapping a global program to one local process per role, in a session-typed asynchronous process calculus.
Operational correspondence: the projected endpoint system is proven to match the choreography step-for-step, so the endpoints inherit the choreography’s deadlock-freedom and communication safety — the guarantee survives distribution.

Connections

Conceptual Contribution

Claim: Deadlock-freedom for distributed, multiparty, multi-session programs should be obtained by design — by programming the protocol globally as a choreography and projecting to endpoints — rather than by per-session typing, because local session types guarantee only intra-session progress and cannot see the cyclic wait-for dependencies that form when one participant interleaves several sessions; a global program is structurally incapable of expressing such a cycle, and a sound endpoint projection transports that guarantee to the distributed implementation.
Mechanism: A global programming (choreography) language over an asynchronous, session-typed process model with message queues; a typing discipline for choreographies that open and interleave multiple multiparty sessions; an endpoint-projection function from global programs to per-role local processes; and an endpoint-projection theorem proving operational correspondence between a well-typed choreography and the parallel composition of its projections, from which the endpoint system’s deadlock-freedom and communication safety follow as corollaries.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, Session Types, global program, session interleaving, Deadlock Freedom, asynchronous π-calculus, communication safety
Stance: foundational / formal-semantic
Relates to: Sequel in the choreography lineage to Structured Communication-Centred Programming for Web Services (Carbone-Honda-Yoshida ESOP 2007 / TOPLAS 2012) and Multiparty Asynchronous Session Types (Honda-Yoshida-Carbone POPL 2008): where those works establish the global-types / local-types / endpoint-projection triangle and guarantee intra-session progress, this paper closes the cross-session deadlock gap by making global programming itself the deadlock-freedom mechanism. Direct ancestor of the production choreographic languages Choral, HasChor and ChoRus, and of the agentic revival in Pact - A Choreographic Language for Agentic Ecosystems; consolidated pedagogically in Introduction to Choreographies (Montesi 2023). The runtime-verification counterpart for the projected endpoints is On the Monitorability of Session Types (Bartolo Burlò et al. ECOOP 2021). The asynchronous π-calculus / Communicating Sequential Processes substrate underlies the endpoint process model.

Tags

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

Model Checking

An automated verification technique that exhaustively explores the state space of a finite model of a system to decide whether it satisfies a temporal-logic specification. It is applied to ACL protocols and blockchain interoperability patterns to expose deadlocks, liveness failures and protocol violations.

In this vault

Duality

(page does not exist)

Global Types

(page does not exist)

Subject Reduction

(page does not exist)

Liveness

(page does not exist)

Deadlock Freedom

(page does not exist)

Behavioural Types

(page does not exist)

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

Choreographic Programming

A programming paradigm in which a single global program describes the joint behaviour of all participants in a distributed protocol, and a mechanical endpoint projection derives the local program for each participant. Choreographic languages are designed so that well-typed choreographies are deadlock-free by construction — every send is matched by a corresponding recv in the projected counterpart. Originating in WS-CDL and formalised in the π-calculus / session-types community (Carbone, Honda, Yoshida), the paradigm has since been embedded in production languages (Choral for Java, ChoRus for Rust, HasChor for Haskell, Bates et al.’s census-polymorphic projection at PLDI 2025) and extended towards adversarial settings via cryptographic primitives (Sarkar & Russo; Veiga). Structurally adjacent to the Commitment-Based Protocol tradition: both specify protocols globally and project to local roles, but choreographic semantics is operational/communicational while commitment-based semantics is normative/social.

In this vault

Endpoint Projection
Structured Communication-Centred Programming for Web Services — Carbone, Honda & Yoshida ESOP 2007 / TOPLAS 2012, the foundational paper
Multiparty Asynchronous Session Types — Honda, Yoshida & Carbone POPL 2008, multiparty generalisation
Deadlock-freedom-by-design - Multiparty Asynchronous Global Programming — Carbone & Montesi POPL 2013, deadlock-freedom by construction across interleaved sessions
Introduction to Choreographies — Montesi 2023 (Cambridge), the canonical textbook
On the Monitorability of Session Types — Bartolo Burlò, Francalanza & Scalas ECOOP 2021, runtime monitoring
Session Types
Pact - A Choreographic Language for Agentic Ecosystems
Commitment-Based Protocol
Commitment Machines
Flexible Protocol Specification and Execution
Algebraic Effects

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

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