A Calculus of Mobile Processes (Parts I and II)

Reference: Milner, R., Parrow, J. & Walker, D. (1992). A Calculus of Mobile Processes, I and II. Information and Computation, 100(1), pp. 1–40 and pp. 41–77. (Reports appeared as ECS-LFCS-89-85 and -86, Edinburgh, 1989.) Companion textbook: Milner, R. (1999). Communicating and Mobile Systems: the π-Calculus. Cambridge University Press. DOI · Open access (Edinburgh)

Summary

Milner, Parrow and Walker introduce the π-calculus, a process calculus in which the names exchanged between processes are themselves the channels of communication. The earlier CCS (Milner 1980) had a fixed communication topology — process structure determined which agents could synchronise. The π-calculus drops that restriction: a single primitive, the output of one name on another (x̄⟨y⟩), simultaneously transmits a capability to communicate and reconfigures the network. The paper develops the calculus in two parts: Part I gives the syntax (input prefix, output prefix, parallel composition, restriction (νx), replication !P, summation +, match [x=y]), the structural-congruence-and-reduction operational semantics, and proves the basic algebraic theory; Part II develops a higher-order extension and the labelled-transition / bisimulation theory (early, late, and open variants of strong and weak bisimulation). The headline expressive result, established in detail in Milner’s companion Functions as Processes (1992), is that the lazy and call-by-value λ-calculi embed faithfully into the π-calculus — concurrent computation strictly subsumes sequential functional computation. The calculus has since become the standard substrate for reasoning about Mobility, Concurrency, and Session Types, and is the formal predecessor of every choreographic / multiparty-session-type result in this vault.

Key Ideas

Name-passing as the unifying primitive: a single output prefix x̄⟨y⟩.P transmits a name y over channel x; the receiver x(z).Q binds z to y and may then use it as a channel — communication and channel reconfiguration become one operation.
Restriction (νx)P: introduces a fresh, private name; combined with output, it gives scope extrusion — when a private name is communicated outside its scope, the scope expands to include the recipient. This is the formal mechanism of mobility.
Replication !P: the calculus’s only recursion construct, equivalent to P | !P; supports unbounded parallelism without an explicit fix-point.
Three bisimulation styles: early (instantiate the bound name before the transition), late (transition on a name-abstraction), open (transitions parametric in a substitution closure) — different congruence properties; open bisimulation is preserved by all contexts.
λ encodes into π: lazy and call-by-value λ-calculi translate compositionally into π, with β-reduction simulated by communication. Sequential function application is a degenerate case of concurrent name-passing.
Polyadic and monadic forms: tuples of names (x̄⟨y₁,…,yₙ⟩) can be encoded into the monadic calculus; this encoding is the basis of Sorts / type systems for π, and of session types.
Single-paper foundation for an entire research programme: Hoare’s CSP and Milner’s earlier CCS supplied process algebra over fixed topologies; π-calculus made the topology itself first-class data.

Connections

Conceptual Contribution

Claim: A single primitive — the communication of names along names — suffices to express both classical concurrency (CCS-style fixed-topology synchronisation) and the dynamic reconfiguration of communication networks; the resulting calculus subsumes the λ-calculus and serves as a universal substrate for mobile, concurrent computation.
Mechanism: Reduction-and-congruence operational semantics over a small syntax (input/output prefix, |, (νx), !, +, [x=y]); scope extrusion as the single rewrite rule that lets restricted names escape their original scope when communicated; early/late/open bisimulation as compositional behavioural equivalences; λ-encoding via continuation-passing-style translation into name communication.
Concepts introduced/used: Pi-Calculus, Name-Passing, Scope Extrusion, Mobility, Bisimulation (early, late, open), Replication, Restriction, Sorts (precursor to session types), Higher-Order Pi-Calculus.
Stance: foundational technical paper / textbook calculus.
Relates to: Direct ancestor of Session Types (Honda et al., where the name being passed carries a type describing how the recipient may use it) and through them of Multiparty Asynchronous Session Types and Structured Communication-Centred Programming for Web Services — the entire choreographic-programming line in this vault, including Pact - A Choreographic Language for Agentic Ecosystems, rests on π-calculus reductions as the underlying small-step semantics. Mobile Ambients (Cardelli & Gordon 1998) is a sibling calculus that makes locations rather than names the primary mobile entity, motivated by the difficulty of expressing administrative domains in pure π. Spi Calculus (Abadi & Gordon 1997) extends π with cryptographic primitives for protocol verification — directly relevant to the agent-security threads. Join Calculus (Fournet & Gonthier 1996) is an asynchronous, join-pattern reformulation amenable to distributed implementation. The encoding of λ into π reframes Hewitt actors as a particular discipline of π usage and supplies the formal grounding for asynchronous-message-passing concurrency in actor-based systems like Erlang. On the agent-communication side π is the missing semantic substrate for Conversation Policy and Interaction Protocols: a KQML/FIPA performative exchange is — operationally — π-calculus name-passing constrained by an ontological vocabulary, a fact made explicit by every session-typed reformulation of ACL conversations.

Tags

#process-calculi #pi-calculus #concurrency #mobility #foundations #milner #bisimulation #session-types-foundation

Backlinks

Linked Pages

Interaction Protocols

Specifications of legal conversation patterns (e.g. as Petri nets or state machines) above the message level.

In this vault

Conversation Policy

Constraints on legal sequences of ACL messages — the layer between single performatives and a full protocol.

In this vault

Programming Erlang Second Edition

Programming Erlang: Software for a Concurrent World (Second Edition)

Reference: Armstrong, J. (2013). The Pragmatic Bookshelf. Source file: cbcl-ref/programming-erlang-2nd-edition.pdf. URL

Summary

Joe Armstrong’s second-edition textbook introduces Erlang as a language and runtime for building highly concurrent, distributed, and fault-tolerant systems. Part I motivates concurrency and tours the shell, modules, and compilation. Part II teaches sequential Erlang: atoms, tuples, lists, pattern matching, funs, records/maps, error handling with try/catch, binaries and the bit syntax, and the type system with Dialyzer.

Part III covers the concurrency primitives (spawn/send/receive), error handling in concurrent programs (links, monitors, supervised fault-tolerance), and distributed programming over Erlang nodes. Part IV covers libraries and frameworks (ports for C interfacing, files, sockets, web/WebSocket applications, ETS/DETS and Mnesia databases, and profiling/debugging/tracing). The book is widely cited as a canonical introduction to the Actor model and the “let it crash” philosophy that informs modern reactive and distributed-agent systems.

Key Ideas

Actor-model concurrency: processes + asynchronous message passing.
“Let it crash” + supervision trees for fault tolerance.
Pattern matching as pervasive control structure.
Distributed programming built on the same primitives as local.
Mnesia, ETS/DETS for in-memory and persistent storage.

Connections

Conceptual Contribution

Claim: Concurrent, distributed and fault-tolerant software is simpler and more reliable when built on isolated processes that share nothing and communicate only by asynchronous messages, with failures handled by supervision rather than defensive programming (“let it crash”).
Mechanism: Armstrong teaches the Erlang trinity of spawn / send / receive, reinforces isolation via immutability and pattern matching, and then layers links, monitors and supervisor trees for systemic recovery. Distribution uses the same primitives as local concurrency, so topology becomes deployment-time. Supporting libraries (ports for C, sockets, ETS/DETS, Mnesia, tracing/profiling, web/WebSocket) show how the model scales to realistic systems.
Concepts introduced/used: Actor Model, Let It Crash, Supervision Tree, Erlang Process, Pattern Matching, Link and Monitor, Mnesia, ETS-DETS, Bit Syntax, OTP
Stance: engineering
Relates to: The practical counterpart to the fault-tolerance philosophy of Theory of Self-Reproducing Automata and the architectural dependability of Architectural Patterns for Dependable Software Systems - SOL; its message-passing primitives underpin agent frameworks surveyed in Intelligent Agents Theory and Practice and mesh with the calculus-level treatment in Secure Communications Processing for Distributed Languages.

Tags

Hewitt's Actor Model

Hewitt’s Actor Model

The original asynchronous-message-passing concurrency model proposed by Hewitt, Bishop & Steiger (1973). An actor is a stateful entity with a mailbox that, in response to a message, may: send a finite number of messages, create a finite number of new actors, and designate the behaviour for the next message. Universally cited as the predecessor of CSP, CCS, the Pi-Calculus, and Erlang; the asynchronous π-calculus and the Join Calculus supply formal accounts of actor-style concurrency that compose with bisimulation theory.

In this vault

Join Calculus

Process calculus (Fournet-Gonthier) based on join patterns — asynchronous receive on multiple channels at once; basis for ML-style distributed languages.

In this vault

Secure Communications Processing for Distributed Languages

Spi Calculus

Abadi & Gordon’s (1997) extension of the Pi-Calculus with cryptographic primitives — encryption, decryption, hashing, pairing, name-equality. Security properties (authentication, secrecy) are formalised as process equivalences: a protocol is secure iff no spi-calculus context can distinguish it from an idealised specification. The most general attacker is just an arbitrary spi process. Foundation under ProVerif / Tamarin and the applied π-calculus (Abadi & Fournet 2001).

In this vault

Mobile Ambients

Reference: Cardelli, L. & Gordon, A. D. (1998). Mobile Ambients. In Foundations of Software Science and Computational Structures (FoSSaCS ’98), LNCS 1378, pp. 140–155, Springer. Journal version: Theoretical Computer Science 240(1), pp. 177–213, 2000. DOI · Open access PDF (UPenn)

Summary

Cardelli and Gordon argue that the Pi-Calculus models communication elegantly but does not natively model administrative domains — the bounded, named, hierarchically nested regions across which computation moves on the actual Internet (firewalls, address spaces, processes, machines, networks). Their ambient calculus makes the location itself the primary mobile entity. An ambient n[P] is a named bounded region containing a process P. A small set of capabilities — in n.P, out n.P, and open n.P — drive movement: in n enters a sibling ambient named n; out n exits the parent ambient if it is named n; open n dissolves the boundary of a child ambient named n, merging its contents with the current location. Communication is local: (x).P reads from a shared anonymous channel within the surrounding ambient. Mobility and access control reduce to one question — does a process possess the capability to cross a particular boundary? The calculus has standard structural-congruence-and-reduction operational semantics, a logical companion (the ambient logic, with location-modal connectives), and type systems regulating mobility. It supplies the formal substrate for reasoning about agents that physically relocate — mobile-code platforms, container migration, and (today) WASM components moving between hosts.

Key Ideas

Locations as first-class movable entities: the basic mobile thing is a named bounded region, not a name-as-channel; this captures administrative-domain structure that pure π struggles to express.
Three capabilities — in, out, open — suffice: every mobility scenario reduces to a sequence of crossings governed by capability possession; access control becomes “do you have the capability name?”
Spatial nesting as syntax: ambient terms form trees n[P | m[Q] | …]; the structural-congruence laws are spatial as well as algebraic. The ambient logic adds location modalities (@n reads “at ambient n”) for spatial reasoning.
Bounded computation: an ambient acts like a bag carrying its computation; its contents proceed concurrently inside the boundary, distinct from the outside world.
Communication restricted to local anonymous channels: a deliberate departure from π’s named channels — values are read off the local “ether” within an ambient. Gives an asymmetric model where mobility is global but communication is local.
Type systems for mobility: subsequent work (Cardelli, Ghelli, Gordon 1999/2000) gives type disciplines that statically constrain which ambients may cross which boundaries — the ancestor of capability-typed mobile-code systems.
Deliberate engineering target: motivated explicitly by Java applets, Telescript-style mobile agents, and firewall-bounded computation — process-calculus theory aimed at the engineering reality of distributed systems.

Connections

Conceptual Contribution

Claim: Modelling internet-scale distributed computation requires a process calculus in which the location is the primary mobile entity, not the channel; three boundary-crossing capabilities (in, out, open) suffice to express administrative-domain mobility, and capability possession is the natural account of access control.
Mechanism: A process language extending π-style parallel composition with ambient brackets n[P] and capability prefixes; small structural-congruence-and-reduction operational semantics; an ambient logic with spatial / location modalities; type systems controlling which ambients can perform which capabilities.
Concepts introduced/used: Mobile Ambients, Ambient Calculus, Capabilities (Ambient), Mobility, Spatial Logic, Boundary (administrative domain).
Stance: foundational technical paper.
Relates to: Sibling of the Pi-Calculus — both Milner 1992 and Cardelli & Gordon 1998 lift CCS-style fixed-topology concurrency, but along different dimensions (channel-mobility vs location-mobility). Conceptually upstream of all capability-based mobile-agent security work in the vault: Agent Tcl Flexible Secure Mobile Agents and DAgents Security Book Chapter take the engineering view, while ambients give the formal model. The capability-as-token view aligns directly with Capability Security (Dennis & Van Horn 1966, Miller’s E lineage in Robust Composition - Towards a Unified Approach to Access Control and Concurrency Control) — possession of a capability name confers, and only confers, the right to act. Modern realisations include WebAssembly modules with WASI capabilities, container ingress/egress, and sandboxed JS with capability-secured imports — a re-discovery of ambient-style boundary control under different syntactic skins.

Tags

#process-calculi #mobile-ambients #cardelli #gordon #mobility #capability-security #foundations

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

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

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

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

Higher-Order Pi-Calculus

A variant of the Pi-Calculus in which processes themselves (not only names) may be communicated. Sangiorgi (1992) proved that higher-order π is reducible to first-order (name-passing) π by a CPS-style encoding — passing a process is operationally equivalent to passing a trigger name together with replicating the process to receive on that name. The reduction shows that name-passing alone is expressively complete; higher-order forms are convenient but not fundamental.

In this vault

Sorts

A simple type discipline over Pi-Calculus names introduced by Milner (1991/1993). A sort assigns to each name a sort tag and to each tag a tuple of sorts that names of that tag may carry. Sorts rule out arity mismatches in name-passing and are the precursor of richer type systems for π — including Session Types, which annotate names not merely with what they carry but with the protocol governing their use.

In this vault

Restriction

The Pi-Calculus operator (νx)P introducing a fresh, private name x whose scope is P. Combined with Name-Passing, restriction enables Scope Extrusion — the dynamic widening of a private channel’s scope when it is communicated outward. Restriction is the calculus’s binder for fresh resources: cryptographic keys, session channels, private references.

In this vault

Replication

The Pi-Calculus operator !P, equivalent up to structural congruence to P | !P — an unbounded supply of copies of P running in parallel. The calculus’s only source of recursive / unbounded behaviour, replacing CCS-style fixed-point definitions. Crucial for encoding services that handle arbitrarily many requests, and for the λ→π encoding (Milner 1992).

In this vault

Bisimulation

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

In this vault

Mobility

In process-calculus terms, the dynamic reconfiguration of a system’s communication topology — links between processes can be created, communicated, and revoked at runtime. The Pi-Calculus gives the canonical formal account through Name-Passing and Scope Extrusion: a private channel may be communicated outside its original scope, expanding the set of processes that can use it. Mobile Ambients (Cardelli & Gordon 1998) takes a different stance — the mobile entity is a location (an ambient) rather than a name. Mobile-agent systems like Telescript and Agent Tcl are the engineering realisations.

In this vault

Scope Extrusion

The structural rewrite of the Pi-Calculus under which a restricted (private) name escapes its original scope when communicated to a process outside that scope. Formally: (νx)(P | Q) ≡ (νx)P | Q when x ∉ fv(Q), combined with the communication of x from P into Q extends the binder to cover both. This is the formal mechanism of Mobility in π — the only rewrite needed to capture all of dynamic-topology concurrent computation.

In this vault

Name-Passing

The defining primitive of the Pi-Calculus: a communication action transmits a name (channel) over another name. Because the transmitted name may itself be used as a channel by the recipient, communication and the dynamic reconfiguration of the communication network become a single operation. Name-passing is what distinguishes π from the fixed-topology process algebras CCS and CSP. In a session-typed setting the name carries a type describing how the recipient may use it — the foundational mechanism behind Session Types and endpoint projection.

In this vault

Pi-Calculus

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

In this vault

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

Process Calculi

A family of formal languages for describing concurrent and distributed systems algebraically. A process calculus fixes a small syntax of process terms (parallel composition, action prefix, restriction, choice) and gives an operational semantics — usually as a labelled transition system — together with a behavioural equivalence such as Bisimulation. Canonical members:

CCS (Milner 1980) — fixed-topology synchronisation.
CSP (Hoare 1978) — synchronous channel rendezvous; refinement-based equivalences.
ACP (Bergstra & Klop 1984) — equational laws as primary; ad-hoc-extensible signature.
π-calculus (Milner, Parrow & Walker 1992) — name-passing; mobile communication topology.
Mobile Ambients (Cardelli & Gordon 1998) — mobile locations.
Join calculus (Fournet & Gonthier 1996) — asynchronous; pattern-matching on joins.
Spi calculus (Abadi & Gordon 1997) — π + cryptographic primitives.
Applied π-calculus (Abadi & Fournet 2001) — equational theories over terms.

Process calculi supply the formal substrate underneath Session Types, Choreographic Programming, and most modern accounts of distributed-system semantics.

In this vault

Lambda Calculus

A formal system introduced by Church that expresses computation via function abstraction and application. It serves as a foundational model of computation and the theoretical basis for functional programming languages.

In this vault

Security Kernel Lambda Calculus
An Unsolvable Problem of Elementary Number Theory — Church 1936, the λ-calculus applied to the Entscheidungsproblem.

Algebra of Communicating Processes

ACP, developed by Bergstra & Klop (1984/1985), is a process algebra in which the equational laws are taken as primary and the operational semantics is derived. Where CCS starts from a labelled-transition system and derives equivalences, ACP starts from an axiom system (associativity / commutativity of +, distributivity of · over +, etc.) and proves that suitable models satisfy it. ACP also pioneered an extensible approach: new operators (priority, encapsulation, abstraction) are added together with their defining laws.

In this vault

A Universal Modular Actor Formalism for Artificial Intelligence

Reference

Hewitt, C., Bishop, P., & Steiger, R. (1973). “A Universal Modular Actor Formalism for Artificial Intelligence.” Proceedings of the 3rd International Joint Conference on Artificial Intelligence (IJCAI), 235-245. URL

Summary

Hewitt, Bishop, and Steiger introduce the Actor — a universal computational primitive that unifies data, procedure, and process under a single kind of object. An actor is an active agent with behavior defined entirely by the messages it sends and receives. All computational structures — numbers, functions, semaphores, cells, queues, interpreters — are modeled uniformly as actors that respond to messages. Control flow and data flow are inseparable; sending a message replaces goto, call-return, interrupt, and semaphore operations with a single mechanism.

The paper grew out of the PLANNER project and explicit dissatisfaction with the von Neumann / stored-program paradigm dominant in AI languages. In place of “program counter + global memory + interrupts,” the actor model offers local state per actor, inherent concurrency via simultaneous message sends, and a coherent account of parallelism that scales from fine-grained numeric computation to large, autonomous agents. The authors emphasize intentions as first-class properties — an actor’s intention is the contract it guarantees to satisfy for its senders, supporting a form of declarative meta-evaluation and debugging.

Hewitt’s framework anticipated and influenced a long arc of subsequent work: Smalltalk’s message-passing object model, Agha’s formalization of actor semantics, Erlang/OTP’s supervised processes and let-it-crash philosophy, the Akka framework, CSP (Hoare) which formalized a closely related but channel-centric style, and contemporary actor-based agentic systems. The paper’s insistence that “creation, control, and communication” are one mechanism remains the defining alternative to shared-memory concurrency.

Key Ideas

Actor = message-receiving agent: a single primitive subsumes data, procedures, processes.
Message passing only: no shared memory, no goto, no interrupt, no semaphore.
Inseparability of control and data: computation is intrinsic — “ask not what you can do to an object; ask what the actor will do for you.”
Inherent concurrency: every message send is potentially parallel.
Intentions / contracts: each actor publishes obligations; meta-evaluators check that behavior satisfies intentions.
Modularity via encapsulation: actors expose only message interfaces; internal state is private.
Universality: the formalism expresses every computational construct needed for AI programming without primitive aggregates.
Hierarchies of scheduling, intention, monitoring, binding, resource management: supervisory structures emerge naturally.

Connections

Actor Model
Programming Erlang Second Edition — the most successful large-scale realization.
Let It Crash
Supervision Tree
A Language-Based Approach To Prevent DDoS
The Society of Mind — Minsky’s agent-of-agents shares the intuition.
Communicating Sequential Processes — Hoare’s contemporary rival formulation.
Hoare Logic

Conceptual Contribution

Actor Model

Hewitt’s concurrency model: isolated actors communicating by asynchronous messages, spawning new actors, and changing local behaviour.

In this vault

Linear Logic

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

In this vault

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

Structured Operational Semantics

SOS, developed by Plotkin (1981, A Structural Approach to Operational Semantics, Aarhus tech report DAIMI FN-19), defines program meaning by inductive rules on syntax that derive a labelled transition relation P --a--> P'. The technique was developed in dialogue with Milner’s CCS programme: SOS is the standard recipe for giving an LTS to a process calculus. Compared to denotational semantics, SOS is amenable to small-step reasoning, easier to extend, and underwrites every modern process-calculus and type-soundness proof.

In this vault

A Calculus of Communicating Systems

Reference: Milner, R. (1980). A Calculus of Communicating Systems. Lecture Notes in Computer Science 92, Springer-Verlag. Companion paper: Milner, R. (1989). Communication and Concurrency. Prentice Hall. Springer (LNCS 92) · Edinburgh Research Explorer (Citation only — book.)

Summary

Milner introduces CCS, the first algebraic process calculus to make synchronisation rather than shared state the foundation of concurrency. A CCS process is built from action prefix (a.P), summation (P + Q), parallel composition (P | Q), restriction (P \ L), relabelling (P[f]), and (constant) recursion. Communication is synchronous handshake between complementary actions a and ā — paired transitions yield a silent τ. The technical heart of the monograph is the development of observational equivalence (later refined by Park into bisimulation) as a behavioural equivalence preserved by all CCS contexts: two processes are equivalent iff they can match each other’s transitions step-for-step. Earlier Milner had developed the equivalence over synchronisation trees — tree unfoldings of the LTS — and shown that CCS is sound and complete for strong equivalence given a finite axiomatisation. The calculus served as the workhorse for ten years of process-algebra research and is the direct predecessor of the Pi-Calculus, which lifted CCS’s fixed-topology assumption by making channel names mobile values. The 1989 Communication and Concurrency book is the more polished re-presentation that most readers cite.

Key Ideas

Synchronous handshake as the primitive: complementary actions on a shared name produce a silent step; concurrency is communication, not interleaving over a heap.
Algebraic, not denotational: the meaning of a CCS term is given by its position in an equational theory under bisimulation, not by translation into a domain. Laws like P + 0 = P, (P | Q) | R = P | (Q | R), and the expansion law (P | Q distributes over a sum of all possible synchronisations) form the calculational kit.
Synchronisation tree: the LTS unfolded as an action-labelled tree; equivalences over LTSs lift to equivalences over trees.
Observational equivalence ≈ bisimulation: invented and refined within the CCS programme; the standard behavioural equivalence ever since.
Restriction P \ L: hides a set of action names from the environment, forcing them to synchronise within P — this is what later inspires π’s (νx) binder, generalised to fresh names.
Recursion via constants: rather than fix-point operators, CCS uses named process equations A ≜ a.A, simpler to manipulate algebraically.
Limitations that motivate π: communication topology is fixed at a process’s birth — there is no way for a.P to communicate b to a peer who could then use b to communicate further. This restriction is exactly what name-passing in π lifts.

Connections

Conceptual Contribution

Claim: Concurrency can be developed as an algebraic theory of synchronisation in which the meaning of a process is determined by an observational equivalence preserved under all contexts; communication, not shared state, is the right primitive.
Mechanism: A small term language (prefix, sum, parallel composition, restriction, relabelling, named recursion); structural-operational-semantics rules deriving a labelled transition system; observational equivalence (≈ bisimulation) preserved by all syntactic contexts, with a complete equational axiomatisation in the finite case.
Concepts introduced/used: CCS, Synchronisation Tree, Observational Equivalence, Bisimulation, Process Calculi, Structured Operational Semantics (developed by Plotkin in dialogue with the CCS programme).
Stance: foundational technical monograph.
Relates to: Sibling of Communicating Sequential Processes (Hoare 1978), which uses an event-trace semantics and refinement orderings rather than bisimulation. Direct ancestor of the Pi-Calculus (A Calculus of Mobile Processes) which keeps the algebraic methodology but lifts the topology restriction. The actor-model line (Hewitt 1973, realised industrially in Erlang) takes asynchronous, mailbox-based messaging as primitive — historically opposed to CCS’s synchronous handshake but reconciled in asynchronous π and the Join Calculus. CCS supplies the underlying behavioural-equivalence machinery used (often implicitly) when reasoning about Conversation Policy equivalence in the ACL literature: two protocols are “the same” iff they bisimulate.

Tags

#process-calculi #ccs #milner #concurrency #foundations #bisimulation #synchronisation

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

Concurrency

The simultaneous progress of multiple computational activities. Different traditions formalise concurrency differently: shared-memory + locks (the von Neumann inheritance), message passing (Actor Model, CSP), process algebra (CCS, Pi-Calculus, Mobile Ambients), dataflow, and lattice-monotonic execution (CALM Theorem). The agent-communication line treats concurrency as the default condition: any sufficiently rich multi-agent system is intrinsically concurrent and distributed, so behavioural equivalences (Bisimulation) and protocol monitorability (On the Monitorability of Session Types) are first-class concerns.

In this vault

CCS

The Calculus of Communicating Systems (Milner 1980) — the first algebraic process calculus in which synchronisation rather than shared state is the foundation of concurrency. CCS processes are built from action prefix, sum, parallel composition, restriction, relabelling, and named recursion; communication is synchronous handshake between complementary actions. The behavioural theory is Bisimulation (a.k.a. observational equivalence). Direct predecessor of the Pi-Calculus, which lifts the fixed-topology assumption.