ChoRus: Library-Level Choreographic Programming in Rust

Reference: Kashiwa, S., Shen, G., Zare, S. & Kuper, L. (2023). Portable, Efficient, and Practical Library-Level Choreographic Programming. arXiv:2311.11472 [cs.PL]. DOI: 10.48550/arXiv.2311.11472. URL. A short version, ChoRus: Library-Level Choreographic Programming in Rust (Kashiwa & Kuper), was presented at CP 2024 (Choreographic Programming workshop, co-located with PLDI 2024). Software: https://github.com/lsd-ucsc/ChoRus.

Summary

ChoRus is the first Choreographic Programming library for Rust. It carries the library-level approach pioneered by HasChor into a language without higher-kinded monadic machinery, and in doing so distils the underlying technique into a language-agnostic recipe. The paper’s first contribution is endpoint projection as dependency injection (EPP-as-DI): rather than compiling a choreography to per-node programs ahead of time, the library bundles the choreographic operators (local computation, communication, etc.) into an interface and injects a node-specific implementation at run time. Projecting the choreography onto a given participant just means running the single global program with that participant’s operator implementations supplied — communications become sends on the projecting node and receives elsewhere. The only host-language feature required is higher-order functions, so the same design transfers to many languages; in Rust the operators are bundled into a trait passed to a run method for an ergonomic API.

The second contribution is choreographic enclaves: a language construct that lets a programmer carve out a sub-choreography among a subset of participants, so that Knowledge of Choice — the obligation to inform every participant affected by a branch — is propagated only within the enclave rather than broadcast to all nodes. This makes branching choreographies more efficient by avoiding unnecessary notifications to participants that are not involved in a local decision. The authors implement both techniques in ChoRus and evaluate it on case studies and benchmarks, finding usability and performance comparable to writing the same distributed systems with conventional Rust libraries — evidence that choreographic programming can be both portable and practical at the library level.

Key Ideas

First CP library for Rust: brings choreographic programming to a systems language, as a library rather than a dedicated compiler.
Endpoint projection as dependency injection (EPP-as-DI): project by injecting node-specific implementations of the choreographic operators into one global program; needs only higher-order functions, hence language-agnostic.
Operators bundled in a trait: Rust realises EPP-as-DI by packaging the choreographic operators into a trait passed to run, giving an idiomatic, ergonomic API.
Choreographic enclaves: sub-choreographies over a subset of participants within which knowledge of choice is propagated only among enclave members, cutting unnecessary selection messages.
Efficiency of branching: enclaves localise the cost of informing participants about choices, improving performance on protocols with local decisions.
Portable & practical: case studies and benchmarks show usability and performance on par with conventional distributed Rust code.
Located values & operator interface: as in HasChor, data is tied to the node that owns it, and communication is the sole operator that moves a value between participants.

Connections

Conceptual Contribution

Claim: Library-level choreographic programming is portable and practical: endpoint projection can be implemented in essentially any language with higher-order functions by treating it as dependency injection of node-specific operator implementations, and branching can be made efficient by scoping knowledge of choice to enclaves of the participants that actually need it.
Mechanism: Express a choreography as one global program parameterised over an interface (a Rust trait) of choreographic operators; project onto a node by injecting that node’s operator implementation and running the program, so communications resolve to sends/receives per participant (EPP-as-DI); introduce choreographic enclaves that delimit a sub-choreography over a participant subset and confine selection/knowledge-of-choice propagation to it; implement and benchmark the design as the ChoRus Rust library.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, endpoint-projection-as-dependency-injection, choreographic enclaves, Knowledge of Choice, located values, Session Types
Stance: language/library design with empirical evaluation
Relates to: The Rust successor to HasChor - Functional Choreographic Programming (Shen, Kashiwa & Kuper ICFP 2023): where HasChor realises endpoint projection as a monadic interpretation in Haskell, ChoRus reframes the same idea as dependency injection so it no longer depends on monads and ports to Rust, adding enclaves for efficient branching. It is a library-level sibling of the compiler-based Choral - Object-Oriented Choreographic Programming (Giallorenzo, Montesi & Peressotti TOPLAS 2024), and both are listed in Introduction to Choreographies (Montesi 2023) as part of the modern implementation landscape building on Structured Communication-Centred Programming for Web Services and Multiparty Asynchronous Session Types. Its enclave mechanism operationalises the realisability condition studied in Knowledge of Choice.

Tags

#choreographic-programming #endpoint-projection #rust #dependency-injection #knowledge-of-choice #session-types #programming-languages

Backlinks

Linked Pages

Knowledge of Choice

Reference: Montesi, F. Knowledge of Choice. Bliki entry, fabriziomontesi.com (created 2023-05-15, updated 2024-12-17). URL. The notion is developed in book form in Introduction to Choreographies (Montesi 2023, Cambridge University Press) and traces to Castagna, Dezani-Ciancaglini & Padovani (2012) and Carbone, Honda & Yoshida (2012); automated repair procedures are given by Lanese, Guidi, Montesi & Zavattaro (2013), Basu & Bultan (2016), and Cruz-Filipe & Montesi (2020, 2023).

Summary

Knowledge of choice is a well-formedness property of choreographies (and, dually, of multiparty Session Types): whenever a participant makes an internal choice between alternative behaviours, every participant whose subsequent behaviour depends on that choice must be made aware of which branch was taken. The property is what makes Endpoint Projection possible — a global choreography can only be projected to deadlock-free local programs if each role can locally determine which branch of a conditional it should follow.

The problem arises when one participant’s private decision silently changes what other participants are supposed to do, without any communication conveying the decision. Montesi’s running example is third-party single sign-on: an authenticator a decides whether a credential is valid, but the web service ws must respond differently depending on that verdict. If the choreography never has a tell ws the outcome, ws cannot know which action to perform, and implementers are pushed toward fragile workarounds — undocumented side-channel messages not reflected in the protocol, or hidden shared state (a common database, side-effects) that breaks the decentralisation the choreography was meant to guarantee.

The standard fix is to add explicit selections — communications that carry a constant value such as a label (OK/KO) — so that every dependent participant can infer the choice from a message it actually receives. In the repaired example, a sends OK or KO to ws, which can then branch locally. Transforming a choreography that lacks knowledge of choice into an equivalent one that has it is called amendment (or repair), and can be performed automatically; the dual mechanism in the projection direction is the merging operator on local types, which decides when two branches of a receiver are reconcilable.

Key Ideas

Definition. When a choice is made between alternative behaviours, all affected participants must be made aware of the choice — otherwise the choreography is not realisable as independent local programs.
Failure mode. A participant’s internal decision affects others’ behaviour, yet no communication conveys the decision, so dependent roles cannot select their branch.
Bad workarounds. Adding undocumented out-of-band messages, or introducing hidden side-effects / shared databases — both break the decentralised, protocol-as-written semantics.
Selections. Communications carrying constant values (labels) inserted so dependent participants can infer the choice locally.
Amendment / repair. A (mechanisable) transformation that inserts the missing selections to restore knowledge of choice while preserving behaviour.
Merging operator. The dual device in projection: it determines when a receiver’s alternative continuations can be merged, i.e. when a role does not need to be told the choice.
Why it matters. Knowledge of choice is a precondition for sound endpoint projection, deadlock-freedom, and communication safety in both choreographies and multiparty session types.

Connections

Conceptual Contribution

Claim: A global protocol is realisable as independent, deadlock-free local programs only if every participant whose behaviour depends on a choice is informed of that choice; “knowledge of choice” names exactly this realisability condition and separates well-formed choreographies from ones that secretly rely on shared state.
Mechanism: Conditionals in a choreography induce a dependency from the deciding role to every role that branches on the decision; the property is satisfied by inserting selections (label-carrying messages), and a choreography lacking it can be amended automatically. Dually, Endpoint Projection uses a merging operator to admit receivers that need not be told.
Concepts introduced/used: knowledge of choice, selection, amendment, merging, Endpoint Projection, Choreographic Programming, Session Types
Stance: foundational / definitional (choreographic-programming theory)
Relates to: The realisability counterpart of Endpoint Projection in Introduction to Choreographies; the property whose violation the choreographic foundations (Structured Communication-Centred Programming for Web Services, Multiparty Asynchronous Session Types) are built to exclude; structurally adjacent to the distributed-knowledge tradition of Knowledge and Common Knowledge in a Distributed Environment, where what an agent must know to act correctly is the central question.

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

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

Introduction to Choreographies

Reference: Montesi, F. (2023). Introduction to Choreographies. Cambridge University Press, Cambridge, UK. ISBN 978-1-108-83376-9 (hardback), DOI 10.1017/9781108981491. 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

Choral - Object-Oriented Choreographic Programming

Choral: Object-Oriented Choreographic Programming

Reference: Giallorenzo, S., Montesi, F. & Peressotti, M. (2024). ACM Transactions on Programming Languages and Systems (TOPLAS) 46(1):1, pp. 1–59. ACM. DOI: 10.1145/3632398. Preprint: arXiv:2005.09520 [cs.PL] (first version 19 May 2020; rev. 19 Oct 2023), DOI: 10.48550/arXiv.2005.09520. URL. Software: https://www.choral-lang.org/.

Summary

Choral is the first choreographic programming language built on mainstream abstractions: it embeds Choreographic Programming into an object-oriented language that compiles to plain Java libraries. Its central technical idea is a new notion of data type parameterised by roles — a type T@(A, B, …) denotes a value whose state is distributed across several participants. An ordinary Java type like Integer@A lives entirely at role A; a type like Pair@(A, B) is a single object whose first component sits at A and whose second sits at B. Choreographies in Choral are simply classes whose methods are parameterised over roles, and an instance of a choreography is an object whose state and behaviour are implemented collaboratively by all of its roles. Interaction between roles happens through channel objects (SymChannel, DiChannel, etc.) whose com method moves a value from one role’s location to another — the only place where a value changes the role it lives at.

The pay-off is endpoint projection realised as ordinary compilation. Given one choreographic class, the Choral compiler generates a separate, compilable Java class for each role — the code that participant actually runs — such that the parallel execution of the projected programs faithfully realises the single global program, deadlock-free by construction. Because the output is idiomatic Java, choreographies compose with existing libraries, run on existing toolchains, and can be published as normal artefacts. Choral is also the first incarnation of choreographic programming to offer real modularity: choreographies support higher-order composition (choreographies passed to and returned from other choreographies), interfaces, subtyping, and generics, so protocols can be abstracted, parameterised, and reused like any other object-oriented code. The paper situates this as the bridge from the multiparty-session-types / choreography theory inherited from Multiparty Asynchronous Session Types and Structured Communication-Centred Programming for Web Services to practical, mainstream software development.

Key Ideas

Roles as type parameters: every Choral type carries one or more roles; Integer@A is data at A, Pair@(A, B) is a single object whose parts are distributed across A and B. Roles are the language’s first-class notion of location.
Choreographies are classes, instances are objects: a choreographic protocol is an OO class parameterised over roles; its methods describe the joint behaviour of all participants, and an object’s state is split across those roles.
Communication via channel objects: com on a typed channel is the sole construct that transfers a value from one role to another — i.e. the only operation that changes where data lives; everything else is ordinary local computation.
Endpoint projection = compilation: the compiler emits one self-contained, runnable Java class per role from a single choreographic source; their concurrent execution realises the global program, deadlock-free by construction.
Mainstream output: generated code is plain Java libraries that interoperate with existing code, build systems, and runtimes — choreographies become ordinary deployable artefacts.
Modularity & higher-order choreographies: choreographies compose via interfaces, subtyping, generics, and first-class choreography values (passed and returned), the first choreographic language to offer such modularity.
Knowledge of choice / selections: branching protocols require that participants affected by a choice be informed of it (via label selection), the projection-level realisability condition shared with Knowledge of Choice and the coherence condition of Multiparty Asynchronous Session Types.

Connections

Conceptual Contribution

Claim: Choreographic programming can be delivered through mainstream object-oriented abstractions rather than a bespoke calculus: by making roles a parameter of data types — so that a single type can describe data distributed across several participants — choreographies become ordinary classes, and endpoint projection becomes ordinary compilation to per-role libraries that are deadlock-free by construction.
Mechanism: Introduce role-parameterised types (T@(R₁, …, Rₙ)) whose values may be distributed across roles; model choreographies as classes whose methods are parameterised over roles and whose instances are objects implemented collaboratively by those roles; restrict cross-role data movement to channel-object com operations; require label selection so that every participant affected by a branch learns of the choice; compile each choreography into one compilable Java class per role (endpoint projection), proving the projected ensemble faithfully and deadlock-freely realises the global program; support higher-order choreographies, interfaces, subtyping, and generics for modular reuse.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, roles, distributed data types, higher-order choreographies, Session Types, knowledge of choice, deadlock freedom
Stance: language design / implementation (with metatheory)
Relates to: The practical realisation of the theory established by Multiparty Asynchronous Session Types (Honda, Yoshida & Carbone POPL 2008) and Structured Communication-Centred Programming for Web Services (Carbone, Honda & Yoshida ESOP 2007 / TOPLAS 2012): where those papers fix the global types → local types → processes pipeline as formal semantics, Choral turns that pipeline into a usable language whose endpoint projection is the compiler and whose output is mainstream Java. It is the reference implementation cited by the textbook Introduction to Choreographies (Montesi 2023) and the canonical “Choral” referenced as a contemporary choreographic-programming language in Multiparty Asynchronous Session Types. Its branching discipline is the realisability property formalised in Knowledge of Choice (Montesi). Pact - A Choreographic Language for Agentic Ecosystems (Gopinathan et al. CP 2026) builds on the same choreographic substrate, adding game-theoretic operators for self-interested agents — where Choral assumes cooperative participants and guarantees correctness by construction, Pact asks why an autonomous agent would follow the projected protocol at all.

Tags

HasChor - Functional Choreographic Programming

HasChor: Functional Choreographic Programming for All

Reference: Shen, G., Kashiwa, S. & Kuper, L. (2023). HasChor: Functional Choreographic Programming for All (Functional Pearl). Proceedings of the ACM on Programming Languages (PACMPL) 7(ICFP), Article 207, ICFP 2023. ACM. DOI: 10.1145/3607849. Preprint: arXiv:2303.00924 [cs.PL], DOI: 10.48550/arXiv.2303.00924. URL. Software: https://github.com/gshen42/HasChor.

Summary

HasChor is a Haskell library that brings Choreographic Programming into a mainstream functional language without a bespoke compiler. A choreography is written as a single global program — an ordinary Haskell computation in a Choreo monad — that describes the behaviour of every participant in a distributed system at once, and the library performs Endpoint Projection at runtime to derive the local program each node actually executes. The library’s central insight, given as a functional pearl, is that endpoint projection has a short and simple essence once it is expressed monadically: the same Choreo value, interpreted with respect to a particular location, naturally specialises to that location’s behaviour, with communications becoming sends on the projecting node and receives on the others.

The interface is built from a small set of choreographic operators — most importantly locally (a local computation at one node) and comm/~> (a directed communication that moves a value from one node to another, returning a located value visible only at the recipient). Located values, indexed by their owning location at the type level, statically prevent a node from using data it does not hold. Because the host language is Haskell, choreographies are first-class and higher-order: they can be passed as arguments, returned, and abstracted over their participating locations (location polymorphism), so reusable distributed protocols compose like ordinary functions. HasChor thus delivers deadlock-free-by-construction distributed code — bank services, key-value stores, and similar examples — entirely as a library, demonstrating that choreographic programming need not be confined to dedicated languages such as Choral.

Key Ideas

Choreographies as a monad: a global program is a value in a Choreo monad; ordinary do-notation expresses the joint behaviour of all participants.
Endpoint projection as interpretation: projection is performed at runtime by interpreting the one Choreo value with respect to a target location — no separate compiler — reducing EPP “to its short and simple essence”.
Located values: a @ l types a value as living at location l; the type system stops a node from accessing data it does not own, enforcing communication safety.
Core operators: locally for node-local computation and comm (~>) for directed communication, which is the only construct that moves data between locations.
Higher-order & location-polymorphic choreographies: choreographies are first-class Haskell values that can be passed, returned, and abstracted over their participants, giving modular, reusable protocols.
Library, not language: the whole approach is a Haskell library, so choreographies interoperate with the existing ecosystem and toolchain.
Functional pearl: the contribution is as much pedagogical as practical — a clean, minimal account of how projection falls out of a monadic embedding.

Connections

Conceptual Contribution

Claim: Choreographic programming can be delivered as an ordinary library in a functional host language rather than a dedicated compiler: once choreographies are embedded as values in a monad, endpoint projection becomes a short runtime interpretation, and choreographies inherit first-class, higher-order, and location-polymorphic composition for free.
Mechanism: Embed global programs in a Choreo monad; type communicated data as located values (a @ l) so the type checker enforces that nodes only touch data they own; provide locally and comm as the core operators; implement endpoint projection by interpreting the single Choreo value against a chosen location, so sends/receives specialise per node; leverage Haskell’s higher-order functions for location-polymorphic, composable choreographies.
Concepts introduced/used: Choreographic Programming, Endpoint Projection, located values, location polymorphism, higher-order choreographies, monadic embedding, Session Types
Stance: language/library design (functional pearl)
Relates to: The library-level counterpart to Choral - Object-Oriented Choreographic Programming (Giallorenzo, Montesi & Peressotti TOPLAS 2024), where Choral makes roles a type parameter and compiles to per-role Java, HasChor keeps endpoint projection inside the host language as a monadic interpretation. It is the direct precursor to ChoRus - Library-Level Choreographic Programming in Rust (Kashiwa et al.), which ports the EPP-as-interpretation idea to Rust as dependency injection. Both are named in Introduction to Choreographies (Montesi 2023) as part of the modern choreographic-programming implementation landscape, and both rest on the choreography/session-type lineage of Structured Communication-Centred Programming for Web Services and Multiparty Asynchronous Session Types.

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

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

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.