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

#choreographic-programming #session-types #multiparty #endpoint-projection #pi-calculus #foundational #type-theory

Backlinks

Linked Pages

Communicating Sequential Processes

Reference

Hoare, C. A. R. (1978). “Communicating Sequential Processes.” Communications of the ACM, 21(8), 666-677. URL

Summary

Hoare proposes that input, output, and concurrent composition of processes deserve the same foundational status as assignment, sequencing, and iteration. CSP is a small language in which programs are built from sequential processes that synchronise by unbuffered, typed message exchange over named channels. A send P ! v and a matching receive Q ? x rendezvous: neither proceeds until both are ready. Dijkstra’s guarded commands — with nondeterministic choice — are generalized so that a guard may include a communication action, yielding a clean treatment of external choice, alternation, and fair scheduling.

The paper walks through a progression of examples — coroutines, prime sieve, matrix multiplication, bounded buffer, recursive subroutines implemented as processes, the dining philosophers — demonstrating how seemingly exotic concurrent patterns become compact CSP programs. Hoare’s deliberate methodological stance is that structured concurrency can be as tractable as structured sequential programming, provided the primitives are well-chosen: synchronous rendezvous avoids the subtleties of mailboxes and shared state; named channels make communication explicit in the program text; guarded commands make nondeterminism principled.

CSP seeded a lineage of enormous practical and theoretical impact: occam (the transputer language), the CSP process algebra (Hoare 1985, Roscoe) with refinement-based verification via FDR, the Go programming language’s goroutines and channels, Rust’s std::sync::mpsc, and the modern “structured concurrency” revival. Together with Hewitt’s actors, CSP defines one of the two great alternatives to shared-memory threads.

Key Ideas

Synchronous message passing: unbuffered rendezvous between named processes; no shared memory.
Named channels / named processes: communication is part of program structure, syntactically explicit.
Guarded commands with I/O guards: nondeterministic alternation and repetition over communications.
Parallel composition (||): processes execute concurrently, synchronizing only at matched send/receive.
No implicit buffering: forces designers to reason about liveness and deadlock directly.
Refinement and equivalence: later formalized as a process algebra with bisimulation / failures refinement.
Structured concurrency: parallelism as a first-class program-structuring mechanism, not threads-as-afterthought.

Connections

Actor Model — the other great message-passing tradition; CSP is channel-centric where actors are mailbox-centric.
A Universal Modular Actor Formalism for Artificial Intelligence
Hoare Logic — Hoare’s earlier work on axiomatic reasoning underlies his insistence on structured primitives.
Time Clocks and the Ordering of Events in a Distributed System — rendezvous provides a stronger local synchrony than Lamport’s messages.
Let It Crash

Conceptual Contribution

Flexible Protocol Specification and Execution

Flexible Protocol Specification and Execution: Applying Event Calculus Planning Using Commitments

Reference: Yolum, P. & Singh, M.P. (2002). Proceedings of the 1st International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS ’02), pp. 527–534. ACM, Bologna. Source file: yolum-singh-2002-flexible-protocol.pdf. URL

Summary

Yolum and Singh argue that finite-state-machine and Petri-net protocol formalisms over-constrain multi-agent interactions because they fix legal sequences of message tokens without regard to what those messages mean. They develop a commitment-based alternative in which each protocol action is reified as an operation on social commitments — Create, Discharge, Cancel, Release, Assign, Delegate — and the rules for how commitments evolve are formalised in a variant of the Event Calculus (Kowalski-Sergot, in Shanahan’s planner formulation). Base-level commitments C(x,y,p) and conditional commitments CC(x,y,p,q) become event-calculus fluents whose Initiates/Terminates clauses constitute the protocol specification.

The running example is the NetBill e-commerce protocol. Three reasoning postulates capture how a base-level commitment is discharged when its content holds, how a conditional commitment resolves into a base-level commitment when its precondition fires, and how CC is consumed when its consequent already holds. An abductive event-calculus planner (Shanahan) is then used to generate protocol runs from an initial state to a goal state, allowing agents to skip steps, reorder messages, or repair exceptions at runtime — provided every base-level commitment created during the run is eventually discharged. The result satisfies Singh’s three social-semantic desiderata: meaningful (content captured), verifiable (compliance checkable from public commitment trace), and declarative (specifies what each action achieves, not how to sequence actions).

Key Ideas

Commitment as fluent in event calculus: C(x,y,p) and CC(x,y,p,q) represented by the EC predicates Initiates, Terminates, HoldsAt, Happens, etc.
Six commitment operations (Create, Discharge, Cancel, Release, Assign, Delegate) compiled into Initiates/Terminates clauses.
Three postulates link content fluents to commitment fluents: discharging on content satisfaction, conditional-commitment resolution, and conditional consumption when consequent already true.
A protocol run is a sequence of Happens events; complete iff no base-level commitment is left holding — incomplete runs identify non-compliant agents.
Abductive planning (Shanahan) generates legal protocol runs from initial-state + goal-state descriptions, restoring autonomy/flexibility lost in FSM models.
Skipping steps and reordering (e.g. send-goods-before-accept) is supported because preconditions are over commitment state, not over a path through an FSM.
Permissions encoded via action preconditions; prohibitions encoded as commitments-not-to-bring-about.

Connections

Conceptual Contribution

Claim: Multi-agent protocols should be specified by the meaning of their actions — concretely, by how each action transforms the agents’ social commitments — rather than by legal token sequences; doing so simultaneously delivers meaningful, verifiable, and declarative semantics, and lets agents skip, reorder, or repair steps via runtime planning while still being held to their obligations.
Mechanism: Reify commitments as event-calculus fluents and define the six manipulation operations (Create/Discharge/Cancel/Release/Assign/Delegate) as Initiates/Terminates clauses; add three reasoning postulates governing base-level discharge and conditional-commitment resolution; use Shanahan’s abductive event-calculus planner to compute runs (sets of Happens clauses with a partial order) from initial states to goal states under the protocol’s preconditions; declare a run complete iff no base-level commitment is left holding, providing an objective compliance criterion.
Concepts introduced/used: Commitment, Conditional Commitment, Commitment-Based Protocol, Commitment-based Semantics, Event Calculus, Abductive Planning, Public Semantics, Verifiable Semantics, Conversation Protocols, Interaction Protocols, NetBill Protocol, Commitment Machines
Stance: formal-semantic / engineering
Relates to: Direct response to FSM- and Petri-net-based protocol traditions critiqued in ACL Rethinking Principles; supplies the operational machinery whose mentalistic counterpart (KQML/FIPA-SL) is shown unverifiable in Verifiable Semantics for ACLs. Companion to Singh’s social-agency programme and to the institutional-reality strand of Agent Communication And Institutional Reality. Conditional-commitment treatment derives from Colombetti’s earlier work and is contemporaneous with A Commitment-Based Approach to Agent Communication (Fornara & Colombetti AAMAS-02 / AAI-04), which gives a complementary object-oriented account of the same primitives (those authors note Yolum-Singh as the closest relative). Commitment-machine compilation to FSMs is the subject of the authors’ parallel ATAL-01 paper. Empire of mentalistic semantics from Intention Is Choice with Commitment is the foil — here intentions/persistence are not needed because the protocol semantics is exhausted by the public commitment trace.

Tags

Commitment Machines - Yolum and Singh

Commitment Machines

Reference: Yolum, P. & Singh, M.P. (2002). Intelligent Agents VIII: Agent Theories, Architectures, and Languages (ATAL-01), LNAI 2333, pp. 235–247. Springer. (A preliminary version appeared in WET-ICE 2000.) Source file: yolum-singh-2002-commitment-machines.pdf. URL

Summary

Yolum and Singh propose commitment machines (CMs) as a protocol formalism that, unlike finite-state machines or Petri nets, attaches declarative meaning to states and actions in terms of the participants’ Social Commitments. A CM is a triple ⟨M, Δ, F⟩ of a finite minimal set of meanings (formulas in a propositional language extended with a commitment operator Cₓp and a strict-implication operator ;), a set of actions ⟨a : e⟩ whose effect e is itself a meaning, and a set of consistent final meanings. Transitions are not enumerated — they are inferred from the logical consequences of applying an action’s effect to the current meaning. The running example is the NetBill Protocol, specified by atomic propositions (request, goods, pay, receipt) and abbreviations for conditional commitments (accept = C_c(goods ; pay), promiseGoods = C_m(accept ; goods), etc.); three reasoning rules govern how commitments evolve as content propositions are made true.

The paper’s central technical contribution is a compilation procedure that turns any complete CM (one whose meaning set is closed under antecedence) into a deterministic FSM that can be executed in constant space without commitment reasoning at run time. The procedure is shown sound (Theorem 2 — every realised computation is generated by the source CM) and complete (Theorem 3 — every CM-generated computation has a semantically-strongest, efficient FSM-realised counterpart from true), via a chain of lemmas about semantic superiority, efficient computations, and endpoint equivalence. Because the meanings of states are explicit, agents executing the CM directly can plan paths through the protocol that exploit opportunities (e.g. a merchant proactively quoting without a request, “try before you buy” deals) and handle exceptions, recovering autonomy that pure-token FSM/Petri-net specifications eliminate.

Key Ideas

Commitment machine ⟨M, Δ, F⟩: state space is a finite minimal set of meanings (formulas) rather than tokens; actions ⟨a : e⟩ carry effect-meanings; final states are a consistent subset of meanings.
Inferred transitions: q ⊨_⟨a:e⟩ r iff (q ∧ e) ⊢ r — transitions are derived from logical entailment, not enumerated edges.
No fixed start state: a CM has no s₀; participants may begin from any meaning whose commitments they accept (typically true).
Three reasoning rules over commitments: (1) Cₓp discharges when p holds; (2) Cₓ(p ; r) collapses to base-level Cₓr when p holds; (3) Cₓ(p ; r) ceases when r holds before p, with no new commitment.
Compilation to deterministic FSM under two restrictions: (R1) no transition mᵢ → mⱼ if mᵢ ⊢ mⱼ (no information-free moves); (R2) the target meaning must dominate all alternatives entailed by the action (forcing maximal information).
Completeness requires “complete” CMs — meaning set closed under antecedence — so that a unique strongest target meaning always exists; trivially achieved by closing under conjunction.
Soundness, completeness, determinism established as theorems over the computation abstraction (sequences of meanings interleaved with actions); computations are compared by semantic superiority and endpoint equivalence rather than literal action-sequence equality.
Flexibility recovered for free: since states encode meanings, agents can skip steps, reorder, or take unsolicited shortcuts whenever the resulting meaning is still in M and the path to a final meaning still exists.

Connections

Conceptual Contribution

Claim: Multi-agent protocols should be specified by giving states and actions declarative meaning in terms of the participants’ commitments — not by enumerating legal token sequences — and any such specification can be soundly and completely compiled to a deterministic FSM, recovering executability without forfeiting flexibility, autonomy, or the ability to handle exceptions and exploit opportunities.
Mechanism: A propositional language with a commitment operator Cₓ and strict-implication ;; meaning sets M and final-meaning sets F (consistent w.r.t. logical consequence); action effects given as meanings; transitions inferred via (q ∧ e) ⊢ r. Compilation Procedure 1 maps ⟨M, Δ, F⟩ → ⟨S=M, Σ={a}, s₀=true, Q=F, δ⟩ under the two information-monotonicity restrictions; Procedure 2 promotes a computation to its semantically strongest counterpart, Procedure 3 removes redundant self-transitions, yielding efficient semantically-strongest computations that are realised by the compiled FSM. Soundness (Thm 2), determinism (Thm 1), and completeness for complete CMs (Thm 3) are proved.
Concepts introduced/used: Commitment Machines, Commitment-Based Protocol, Commitment-based Semantics, Conditional Commitment, Social Commitment, Public Semantics, Verifiable Semantics, NetBill Protocol, Endpoint Projection (structural analogue), Conversation Protocols, Speech Act Theory
Stance: formal-semantic / engineering
Relates to: Direct precursor and structural sibling of Flexible Protocol Specification and Execution (Yolum & Singh, AAMAS-02), which lifts the same six commitment operations (Create / Discharge / Cancel / Release / Assign / Delegate) into the Event Calculus and adds an abductive planner; ATAL-01 here is the FSM-compilation half of that programme. Companion to A Commitment-Based Approach to Agent Communication (Fornara & Colombetti, AAMAS-02 / AAI-04), which gives an OO/FSM operational semantics for the same primitives plus a precommitment state for directives. Carries forward the social-agency programme of ACL Rethinking Principles (Singh 1998) and answers Wooldridge’s challenge in Verifiable Semantics for ACLs by grounding meaning in publicly-observable commitment formulas rather than agent mental state. The Discussion explicitly contrasts with Smith et al.’s joint-intention–based protocols (mental constructs vs. social constructs) — the same fork that Intention Is Choice with Commitment anchors on the mental side. Structurally a direct analogue of choreographic Endpoint Projection: both compile a globally-specified protocol artefact to a per-role executable, the CM/FSM compilation losing declarative meaning for runtime efficiency much as endpoint projection loses the global view for distributable execution. This makes ATAL-01 the load-bearing reference for the constructive synthesis suggested in the Pact - A Choreographic Language for Agentic Ecosystems entry — choreographies could carry both communication structure (Pact-side) and a CM-style commitment trace (Singh-side), with one compilation step yielding both deadlock-freedom and conformance-checkability.

Tags

Pact - A Choreographic Language for Agentic Ecosystems

Pact: A Choreographic Language for Agentic Ecosystems

Reference: Gopinathan, K., Feser, J., Naim, M., Tavares, Z. & Bingham, E. (2026). 2nd International Workshop on Choreographic Programming (CP 2026), Boulder, CO, June 15–19. arXiv:2605.03143v1 [cs.PL], 4 May 2026 (talk paper). Basis Research Institute. URL

Summary

Gopinathan et al. extend Choreographic Programming to the open-systems setting where participants are self-interested and may not faithfully execute a protocol. Choreographies (Montesi 2023; Bates et al. 2025) give correct-by-construction, deadlock-free distributed protocols by writing one global program that is mechanically projected to local endpoints, but they assume cooperative participants — they cannot answer why an autonomous agent should follow the projected protocol. Pact answers that question by adding three operators to a core choreographic calculus: agent.choose(τ) for explicit strategic non-determinism, agent.values(x) for declared utility dependencies, and world.choose(τ) for exogenous “nature” variables that capture each agent’s priors over the environment. Every Pact program then maps unambiguously to a formal extensive-form game.

The headline analysis is a decision-policy solver built on the Memo Programming Language (Chandra et al. 2025), a probabilistic-programming DSL for cognitive theory-of-mind models. From the projected Pact program a memo model is constructed in which each role recursively simulates the other to depth ℓ; running inference yields a level-ℓ bounded-rational policy mapping observations to choices. Applied to the canonical book-seller choreography the solver recreates Akerlof’s Market for Lemons: at depth 0 the buyer naïvely treats price as a signal of quality and the seller exploits this; as ℓ grows the acceptance probability flattens. The implementation is an embedded Python DSL on top of the Effectful algebraic-effects library, with endpoint projection realised as effect handlers. The paper is positioned as preliminary work; next steps named are formalising the semantics, proving correctness of projection-to-game, and adding incentive-compatibility / equilibrium / mechanism-design analyses.

Key Ideas

Choreography + game theory: a global protocol gets three game-theoretic operators (choice, value, nature) so that endpoint projection produces both a runnable program and a formal game.
values as type signature, not utility: declarations name the variables that influence an agent’s payoff but not the function — utilities are private and adversarially incentive-incompatible to disclose. The role of values is to constrain which protocols are mutually negotiable.
Theory-of-mind solver via memo: bounded-rational level-ℓ recursion over agent models, with the recursion bottoming out at naïve priors at ℓ = 0.
Lemons re-derived from a choreography: information asymmetry over an exogenous book.quality variable is enough to reproduce Akerlof’s unravelling result on the bookseller protocol.
Algebraic-effects implementation: endpoint projection implemented as effect handlers in Python (effectful); choreography is a single program that runs differently depending on which handler (Endpoint Projection) is installed.
Motivation framed against LLM agent failure modes: prompt injection, sycophancy, and coercion of LLM agents are cited as the reasons untrusted-counterpart coordination needs formal protocol artefacts rather than free-form natural-language negotiation.

Connections

Conceptual Contribution

Claim: Choreographic protocols for autonomous-agent ecosystems should make agent strategy first-class — explicit choices, declared utility dependencies, and exogenous priors — so that every protocol corresponds to a formal game and can be analysed for whether self-interested agents will participate.
Mechanism: Three new constructs added to a core choreographic calculus (agent.choose, agent.values, world.choose); a structural map from Pact programs to extensive-form games; a level-ℓ bounded-rational decision-policy solver built by translating the projected program into a Memo Programming Language theory-of-mind model and running probabilistic inference over it; an embedded-DSL implementation in Python via algebraic effects realising endpoint projection.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, Theory of Mind, Memo Programming Language, Bounded Rationality, Market for Lemons, Mechanism Design, Algebraic Effects, Negotiation, Game-Theoretic Trust, Mentalistic Semantics
Stance: position / preliminary engineering (CP 2026 workshop talk paper)
Relates to: A contemporary LLM-era restatement of the individual-rationality answer to “why follow a protocol?” first formalised by Deals Among Rational Agents (Rosenschein & Genesereth 1985) and lifted to mental attitudes by Intention Is Choice with Commitment (Cohen & Levesque 1990). The paper is structurally adjacent to — but does not engage — the entire commitment-protocol tradition: Flexible Protocol Specification and Execution (Yolum & Singh 2002) gives a global protocol semantics in the Event Calculus with explicit Create / Discharge / Cancel / Release / Assign / Delegate operations whose runs project to local agents in a way directly analogous to choreographic endpoint projection, and A Commitment-Based Approach to Agent Communication (Fornara & Colombetti 2004) gives an operational FSM semantics for the same primitives. ACL Rethinking Principles (Singh 1998) and Verifiable Semantics for ACLs (Wooldridge 1998) anticipate the central limitation: a semantics grounded in agent utilities and recursive belief models is unverifiable from message traces alone — the very failure modes the paper opens with (prompt injection, sycophancy, coercion) destabilise the priors and rationality assumptions the solver depends on. The Lemons demo, taken at face value, is an argument for institutional / commitment mechanisms (warranties, refund obligations, certification) of the kind Singh’s programme articulates rather than for theory-of-mind solving. The constructive synthesis the paper does not propose is to layer commitment operations onto the choreographic substrate so that protocols carry both a public, observable commitment trace (Singh-style verifiability) and a game-theoretic acceptability analysis (Pact-style strategic reasoning); choreographies are a particularly natural host because endpoint projection already gives the global-to-local move that Commitment Machines approximates by FSM compilation. On the LLM-agent side the paper’s diagnosis converges with Why AI Agents Communicate In Human Language (formal protocol artefacts beat free-form natural-language negotiation) and complements the standardisation argument of LLM Agent Communication Protocol Requires Urgent Standardization.

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

Introduction to Choreographies

Reference: Montesi, F. (2023). Introduction to Choreographies. Cambridge University Press, Cambridge, UK. ISBN 978-1-108-47744-7 (hardback). URL. Citation-only entry; the book is paywalled and the local vault does not hold a source PDF.

Summary

Montesi’s Introduction to Choreographies is the first textbook-level treatment of Choreographic Programming. It develops the field systematically from process-calculus foundations (CCS, π-calculus) through binary and multiparty Session Types to fully-fledged choreographic calculi and their compilation to distributed implementations via Endpoint Projection. The book is organised around the correspondence theorem — the result that a well-formed choreography is bisimilar to the parallel composition of its endpoint projections — and chapters incrementally build the language features (asynchrony, recursion, higher-order communication, knowledge of choice, dynamic participants) needed to express real protocols while preserving deadlock-freedom and communication safety by construction. Worked examples include classic protocols (bookseller, two-buyer, third-party authentication) implemented as choreographies and then projected to executable code.

The book is the canonical contemporary reference and the natural starting point for any reader entering the choreographic-programming literature; it is the primary background that Pact (Gopinathan et al. CP 2026) cites for choreographic programming as such, and the bridge from the foundational papers (Structured Communication-Centred Programming for Web Services, Multiparty Asynchronous Session Types) to the modern implementation landscape (Choral, HasChor, ChoRus). Held in the vault primarily as an authoritative pointer rather than a paper-summary entry.

Connections

Conceptual Contribution

Claim: Choreographic programming has matured to the point where a single textbook can present the field as a coherent discipline — process calculi, session types, choreographic calculi, projection, and implementation — with the correspondence theorem (well-formed choreography ≡ parallel composition of its projections) as the organising spine.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, Session Types, correspondence theorem, knowledge of choice, asynchrony
Stance: textbook / canonical reference
Relates to: The pedagogical synthesis of Structured Communication-Centred Programming for Web Services (Carbone-Honda-Yoshida 2007/2012) and Multiparty Asynchronous Session Types (Honda-Yoshida-Carbone POPL 2008) plus the subsequent decade of work; the natural entry point for understanding Pact - A Choreographic Language for Agentic Ecosystems in lineage. Companion to other foundational textbook references in the vault such as Foundations of Logic Programming - Lloyd.

Tags

#choreographic-programming #textbook #session-types #foundational #citation-only

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

Conversation Protocols

Stateful, multi-turn interaction patterns (Contract Net, auction, query) specified as a finite automaton, Petri net, or role-based dialogue over performatives. Promote tractable ACL use by constraining expected message sequences, and are the unit on which ACRE’s reasoning engine operates.

In this vault

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
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