Linear Logic

Reference: Girard, J.-Y. (1987). Linear Logic. Theoretical Computer Science, 50(1), pp. 1–101. DOI · ScienceDirect (open archive)

Summary

Girard introduces linear logic by stripping the structural rules of weakening and contraction from classical and intuitionistic sequent calculus, then re-introducing them in a controlled way through exponential modalities ! (“of-course”) and ? (“why-not”). The resulting system is resource-aware: a hypothesis can be used exactly once unless explicitly marked reusable. The connectives split into two families — multiplicatives ⊗ (tensor, “with both available”) and ⅋ (par, “the disjunction with both still possible”) and additives & (with, “I choose”) and ⊕ (plus, “the world chooses”) — together with their units, negation as involution, and exponentials. The technical heart is proof nets: a graph-theoretic syntax that quotients away the inessential commutation steps of sequent calculus and gives a strongly normalising calculus of proofs. Cut elimination produces an algorithmic dynamic on proof nets that is the linear analogue of β-reduction. The deep consequences run in two directions: (i) classical/intuitionistic logic embeds into linear logic via the exponentials, so linear logic is a refinement, not a competitor; (ii) the multiplicatives correspond directly to concurrent communication (a two-place tensor is a synchronisation point), making linear logic the formal substrate of a Curry–Howard correspondence for Session Types and π-calculus communication. The paper inaugurated 35+ years of substructural logic, type-theoretic concurrency, and resource-typed programming.

Key Ideas

Resources, not propositions: a linear hypothesis is used, not just consumed in a proof — closer to physical resources or messages than to mathematical truth.
Multiplicatives vs additives: A ⊗ B means “I have both A and B” (independent resources); A & B means “I have a choice between A and B but only one”; A ⅋ B is the multiplicative dual to ⊗; A ⊕ B is the additive sum.
Exponentials reintroduce structural rules locally: !A is a reusable A; weakening and contraction apply to formulas under !; ?A is its de Morgan dual.
Involutive negation: (A^⊥)^⊥ = A syntactically; classical-style symmetry without classical-style proof multiplicities.
Proof nets: cut-elimination becomes graph rewriting; “essentially the same” sequent-calculus proofs become literally the same net.
Curry–Howard for concurrency: linear-logic propositions ⇔ session types; proofs ⇔ processes; cut elimination ⇔ communication. The Caires–Pfenning correspondence (2010) and Wadler’s Propositions as Sessions (2012) turn this into a typed Pi-Calculus in which deadlock-freedom and session fidelity follow from cut elimination.
Light fragments and complexity: Girard’s later light/elementary linear logics (LLL, ELL) capture polynomial-time and elementary computation respectively — proof-theoretic characterisations of complexity classes.

Connections

Conceptual Contribution

Claim: Removing weakening and contraction from sequent calculus and reintroducing them through controlled exponential modalities yields a resource-aware logic that is simultaneously a refinement of classical/intuitionistic logic and the natural type discipline for concurrent, resource-sensitive computation.
Mechanism: Sequent calculus over multiplicative (⊗, ⅋), additive (&, ⊕), and exponential (!, ?) connectives with involutive negation and per-rule resource discipline; proof nets as cut-elimination-amenable graphical syntax; cut elimination as the dynamics of proofs; embeddings of classical and intuitionistic logic via exponentials.
Concepts introduced/used: Linear Logic, Multiplicative-Additive, Exponential Modalities, Proof Nets, Substructural Logic, Curry-Howard Correspondence (concurrent extension).
Stance: foundational technical paper.
Relates to: Provides the type-theoretic substrate that turns the Pi-Calculus from an untyped calculus into a typed one whose well-typed processes are deadlock-free and session-faithful — Caires & Pfenning (2010) and Wadler (2012) make this explicit. Every later session-typed language (Multiparty Asynchronous Session Types, the choreographic-programming languages of Structured Communication-Centred Programming for Web Services and Pact - A Choreographic Language for Agentic Ecosystems) inherits this connection. Outside concurrency, linear logic underlies Rust-style ownership types, region-based memory management, separation logic, and the linear-types extension that landed in Haskell — all engineering descendants of Girard’s resource discipline. Conceptually relevant to Capability Security: a capability is a linear resource (forgeable copies break it), and substructural type systems that prevent capability duplication realise the Dennis–Van Horn ideal in a typed setting; this connection is exploited in modern capability-typed languages (Pony’s reference capabilities, Project Verona, Rust’s borrow checker).

Tags

#linear-logic #girard #substructural #proof-theory #foundations #curry-howard #session-types-foundation

Backlinks

Proof-Carrying Code - Necula
Linear Logic ×2
An Axiomatic Basis for Computer Programming - Hoare
A Calculus of Mobile Processes
index
Substructural Logic ×2
Proof Nets ×2
Multiplicative-Additive ×2
Exponential Modalities ×2
Curry-Howard Correspondence ×2

Linked Pages

Capability Security

Access-control style where authority is conveyed by unforgeable object references; lexical scope in languages like Scheme suffices as a capability kernel.

In this vault

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

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

Curry-Howard Correspondence

The deep structural identity between proofs and programs (Curry 1934, Howard 1969): propositions correspond to types, proofs to programs, and proof normalisation to program execution. The intuitionistic logic / simply-typed λ-calculus correspondence is the classical case. Linear-logic Curry–Howard (Caires & Pfenning 2010, Wadler 2012) extends the correspondence to concurrency: Linear Logic propositions ⇔ Session Types, proofs ⇔ Pi-Calculus processes, cut elimination ⇔ communication. The result is a typed concurrent calculus in which deadlock-freedom and session fidelity are corollaries of cut elimination.

In this vault

Substructural Logic

A logic obtained by removing one or more of the structural rules of sequent calculus (weakening, contraction, exchange). Linear Logic removes weakening and contraction; affine logic keeps weakening; relevant logic keeps contraction; ordered logics also remove exchange. Substructural systems make hypotheses behave like resources, the type-theoretic foundation of ownership types (Rust, Pony’s reference capabilities), region-based memory management, and capability-typed languages.

In this vault

Proof Nets

A graph-theoretic syntax for proofs in Linear Logic introduced by Girard (1987). Where sequent calculus represents inessentially-distinct proofs as different proof trees (differing only in the order of independent rule applications), proof nets quotient that bureaucracy away — “morally the same” proofs become literally the same net. Cut elimination becomes graph rewriting and is strongly normalising. Proof nets are the linear-logic analogue of natural deduction; the corresponding dynamics is the formal counterpart of communication in concurrent Curry–Howard correspondences for Session Types.

In this vault

Linear Logic

Exponential Modalities

The Linear Logic connectives ! (“of-course”) and ? (“why-not”) that re-introduce the structural rules of weakening and contraction in a controlled way: a formula !A is a reusable hypothesis. The exponentials are how classical and intuitionistic logic embed into linear logic — they restore non-linear reasoning locally rather than globally. In the Curry–Howard counterpart for concurrency, !A corresponds to a replicated / shared service: a session offering arbitrarily many copies of A.

In this vault

Multiplicative-Additive

The two families of Linear Logic connectives. Multiplicatives — ⊗ (tensor, “I have both”), ⅋ (par, multiplicative disjunction), units 1 and ⊥ — distribute resources between proofs. Additives — & (with, “I choose”), ⊕ (plus, “the world chooses”), units ⊤ and 0 — share the same context across alternatives. The split corresponds in the Curry–Howard counterpart for concurrency to parallel composition / channel use (multiplicatives) versus internal/external choice (additives) in Session Types.

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

Robust Composition - Towards a Unified Approach to Access Control and Concurrency Control

Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control

Reference

Miller, Mark Samuel. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD Dissertation, Johns Hopkins University, May 2006. Advisor: Jonathan S. Shapiro. Readers: Scott Smith, Yair Amir. URL

Summary

Mark Miller’s dissertation is the foundational synthesis of the object-capability tradition. It argues that the act of composing separately written programs so that they cooperate rather than destructively interfere is the fundamental problem that has limited the scale and functionality of software systems. The thesis proposes a unified framework that binds together access control and concurrency control as two faces of the same compositional discipline: each message send is at once an authority-propagation event and a concurrency-interleaving event, and both must be disciplined together if we are to compose code written by mutually suspicious authors on mutually suspicious machines.

Miller extends decades of object-oriented progress from its comfortable setting (sequential, single-machine, benign components) to the hostile general case: concurrent, distributed, and potentially malicious components. The vehicles for this are the E programming language - a distributed, persistent, object-capability language built around vats, near/far references, eventual-send, promise pipelining, and CapTP - and CapDesk, a virus-safe desktop built in E. Together E and CapDesk form working embodiments of the thesis: authority is only granted by reference-passing along the message graph, and concurrency hazards (deadlock, non-determinism, plan interference) are tamed by the communicating-event-loop / vat model rather than by shared-memory locks.

The dissertation pulls together and formalises the lineage from Dennis & Van Horn, Hardy’s confused deputy, KeyKOS/EROS, Actor-model eventual send, and the SPKI/Granovetter diagram tradition, and it is by far the most-cited reference for object-capability security. Its substantive chapters cover attenuating authority, distributed concurrency control, promise pipelining, the “excess authority as gateway to abuse” argument, and the POLA design discipline.

Key Ideas

Unification of access and concurrency control: both are consequences of disciplining what one object can do to another across a message send.
Object-capability model: authority == what references you hold; “only connectivity begets connectivity.”
Vats and communicating event loops: each vat is a single-threaded turn-taking event loop; cross-vat calls are eventual sends returning promises.
Promise pipelining: chained messages to not-yet-resolved promises reduce round-trips and compose naturally as plans.
CapTP: the cryptographic capability transport protocol that preserves object-capability semantics across mutually-suspicious machines.
Defensive consistency: an object defends its own invariants against arbitrary clients.
POLA as design discipline: hand out only the authority actually needed for each delegation.
CapDesk: demonstrates that a virus-safe desktop is achievable by threading object-capabilities through the UI/shell layer (powerboxes, caplets).

Connections

The Heart of Spritely - Distributed Objects and Capability Security - Spritely is the direct modern successor carrying Miller’s E design forward into Goblins/Guile.
E Language - E is the concrete language Miller designs and evaluates here.
CapTP - Miller’s distributed capability transport, specified in detail.
Capability Security and Object Capability Security - this thesis is the canonical statement of the ocap model.
Ambient Authority - Miller’s thesis is the source of the modern critique of ambient authority.
Confused Deputy - Miller reframes Hardy’s confused-deputy problem as a composition failure.
Principle of Least Authority - POLA is given its definitive formulation here.
Distributed Security - the thesis generalises ocap security to distributed settings.
Security Kernel Lambda Calculus - close kin in the formal-ocap tradition.
A Universal Modular Actor Formalism for Artificial Intelligence - the Actor model is one of E’s direct intellectual ancestors.
Actor Model - vats and eventual sends are the ocap-refined descendants of Hewitt’s actors.
Vat Model - the vat abstraction is introduced and justified here.
Promise Pipelining - Miller gives the definitive account of pipelining in this thesis.

Conceptual Contribution

Algebraic Effects

A programming-language abstraction for structured side-effects: a program declares the effect operations it may perform (e.g. send, recv, choose), and a separately written effect handler gives those operations a concrete interpretation. The decoupling lets the same program run with different handlers — sequentially, in parallel, in a simulator, or projected to a particular role. In Choreographic Programming this is a natural way to realise Endpoint Projection: the choreography is one program, and projection to each role is just installing that role’s handler. Pact’s Python implementation uses Basis Research’s effectful library to implement projection this way.

In this vault

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

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

A Calculus of Mobile Processes

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