Propositions as Sessions: What Armstrong Built and Wadler Proved

Feb 26, 2026

erlangbeamlinear-logicsession-typesconcurrencyresearchkokoelixir

Joe Armstrong started with a practical problem: telephone exchanges that handle 100,000 simultaneous calls cannot go down. Phil Wadler started with a theoretical question: what happens when you take the Curry-Howard correspondence — propositions are types, proofs are programs — and extend it to concurrent processes?

They arrived at the same place from opposite directions. I’m interested in that convergence because I’m running a real experiment to test whether BEAM’s runtime model actually delivers on its promises for agent infrastructure. The theory matters because it tells me what guarantees are even possible.

Armstrong’s path: fault tolerance first

Armstrong joined Ericsson’s computer science lab around 1985. The problem wasn’t concurrency — it was fault tolerance. But the problem domain was inherently concurrent. 100,000 people on a telephone exchange means 50,000 pairs talking simultaneously. The natural model is one process per call.

He tried Smalltalk first. Objects and messages felt right, but Smalltalk had no real failure model and wasn’t truly concurrent. Then Prolog — powerful logic, but when a computation fails you just get “No.” Not exactly useful for keeping a phone network alive.

Over four years (1985–1989), Armstrong, Robert Virding, and Mike Williams evolved Prolog into something new. The language they built had three things that had to be fast at the VM level: message passing, context switching, and error handling. Everything else — supervision trees, leadership election, distributed consensus — could be libraries. But those three primitives had to be in the bone.

The breakthrough primitive was Mike Williams’ idea: links. You link two processes together. If one dies, the other gets a message saying so. That’s it. One mechanism. From that single primitive, they built everything — supervision trees, application structures, the entire fault tolerance story that makes Erlang what it is.

There’s a moment Armstrong describes from a 1990 conference in Bournemouth on distributed systems. After every talk, the Ericsson team would ask the same embarrassing question: “What happens if one of the nodes fails?” Every presenter said they assumed nodes don’t fail. The Ericsson team sat there thinking they were either crazy or the rest of the world was wrong.

They weren’t crazy.

Wadler’s path: propositions as types, extended

Phil Wadler’s work sits in a tradition that goes back to the 1930s. Church’s lambda calculus, Gentzen’s natural deduction, and the discovery that propositions in logic correspond to types in programming — the Curry-Howard correspondence. If you have a proof of a proposition, you have a program of that type. This isn’t a metaphor. It’s an isomorphism.

The question Wadler pursued: can you extend this correspondence to concurrent programs?

The answer came through linear logic, introduced by Jean-Yves Girard in 1987. Classical logic lets you use a proposition as many times as you want. Linear logic treats propositions as resources — use it once and it’s consumed. This maps naturally to communication channels: you send a message on a channel, and the channel’s state changes. You can’t pretend you didn’t send it.

In his 2012 paper “Propositions as Sessions”, Wadler presented two calculi:

CP (Classical Processes): a process calculus where types are propositions of classical linear logic. Every communication protocol is a logical proposition. Every process that follows the protocol is a proof.

GV: a linear functional language with session types — closer to what a programmer would actually write. Wadler gave a translation from GV into CP, formalizing the connection between practical session-typed programming and the underlying logic.

The result that matters: deadlock freedom follows from the correspondence to linear logic. If your program type-checks in this system, it cannot deadlock. Not “probably won’t under normal conditions.” Cannot. The logic forbids it.

Where the paths cross

Armstrong’s processes with links and Wadler’s propositions as sessions solve the same fundamental problem: how do you make concurrent communication safe?

Armstrong solved it pragmatically. Processes are isolated. They communicate only through messages. If something goes wrong, links propagate failure signals. Supervisors restart what died. The philosophy is “let it crash” — don’t try to prevent every failure, build a system that recovers from any failure. This works extraordinarily well in practice. Ericsson’s AXD 301 ATM switch achieved nine nines of availability (31 milliseconds of downtime per year).

Wadler solved it logically. Communication channels have types that describe the protocol — what gets sent, in what order, with what responses expected. Linear types ensure channels are used exactly once (no double-sends, no forgotten receives). The logic guarantees deadlock freedom and protocol compliance at compile time.

These aren’t competing approaches. They’re complementary layers:

Armstrong gives you runtime resilience. When things go wrong (and they will), the system recovers. Links, supervisors, hot code reload, preemptive scheduling — all runtime mechanisms.

Wadler gives you compile-time correctness. Before things go wrong, prove they can’t go wrong in certain specific ways. Session types guarantee protocol compliance and deadlock freedom statically.

Wadler himself collaborated directly with the Erlang world — he and Simon Marlow wrote “A practical subtyping system for Erlang” at ICFP 1997. There’s a wonderful anecdote from an interview where Wadler saw Erlang’s hot code reload — two versions of the same module running simultaneously with all the same function names — and didn’t believe it was possible until they demonstrated it live.

How this applies to what I’m building

I’m running a specific experiment right now: Koko, an Elixir/OTP application that lives alongside my TypeScript agent infrastructure (JoelClaw) and gradually picks up real work. Not a migration — a co-resident proving ground.

The Armstrong/Wadler convergence maps directly onto the architectural decisions I’m making.

The Redis bridge is an informal session protocol

Koko’s Redis bridge protocol defines three phases of communication between the TypeScript stack and the Elixir stack:

Phase 1: Koko passively observes pub/sub events (read-only)
Phase 2: Dedicated channels — joelclaw:koko:events for inbound work, joelclaw:koko:results for outbound results
Phase 3: Bidirectional — Koko emits events back to the gateway

That’s a session type. Phase 1 is a receive-only channel. Phase 2 introduces a request-response pattern with dedicated channels for each direction. Phase 3 is full duplex. The progression from passive observer to active participant is exactly the kind of protocol evolution that session types formalize.

Right now this protocol is enforced by convention and code review. “Koko must not drain the LPUSH list” is a comment in an ADR, not a type constraint. Wadler’s framework suggests this could be a compile-time guarantee — the type system could make it impossible for Phase 1 Koko to write to the wrong channel. Whether Elixir’s type system (or Dialyzer, or a future session-typed Elixir) can actually express this is an open question.

Shadow execution is dual-trace comparison

The shadow executor pattern — where Koko runs the same workloads as TypeScript in parallel and we compare results — has a direct connection to Wadler’s CP/GV duality.

In Wadler’s system, CP (processes) and GV (functional) are two representations of the same computation, connected by a translation that preserves behavior. Shadow execution is the empirical version of this: two implementations (TypeScript and Elixir) of the same function, same inputs, and we verify they produce equivalent outputs.

The shadow rules from ADR-0118 enforce the same invariant that session types enforce logically:

Shadow never writes to authoritative state (no side effects leak across the boundary)
Shadow reads are fine (observation doesn’t mutate)
Shadow failures are data, not incidents (one side crashing doesn’t affect the other)

That’s process isolation. Armstrong’s version: “If Koko crashes, nothing breaks.” Wadler’s version: the types guarantee the shadow channel can’t interfere with the authoritative channel because they’re separate sessions.

Supervision trees are runtime session recovery

Here’s where it gets interesting. Session types guarantee deadlock freedom — but what happens when a process crashes? Linear logic doesn’t model crashes. It models correct programs.

Armstrong’s links fill exactly this gap. A supervisor linked to a worker process gets notified on crash and restarts it. The restarted process can resume the session from a known state (or start a fresh one). Supervision trees are the runtime complement to session types: types prevent protocol violations, supervisors recover from everything else.

Workload 1 — Koko’s health pulse — is the simplest test of this. Three GenServers, each pinging a different service (Redis, Typesense, Inngest). Deliberately crash one. The supervisor restarts it. The other two continue unaffected. This is Armstrong’s link primitive in action — the same mechanism that kept Ericsson’s phone switches alive.

The TypeScript equivalent is my three-layer watchdog: launchd monitors the process, the process monitors its connections, and Inngest monitors the whole thing externally. Three tools bolted together to approximate what one OTP supervisor tree does natively.

Agent communication needs session discipline

The deeper connection: agent systems are concurrent communicating processes with protocols. When my gateway routes a message from Telegram to a pi session, there’s an implicit protocol — send user message, receive assistant response, route response back to source channel. When an Inngest function fans out to sub-steps, each step has a contract about what it receives and what it returns.

None of these protocols are typed. They’re enforced by convention, tests, and hope. A malformed event payload silently does the wrong thing. A step that returns the wrong shape gets caught at runtime (maybe) or produces garbage (definitely).

Session types offer a path where these inter-agent protocols are checked before deployment. The gateway-to-session protocol becomes a session type. The Inngest event-to-function contract becomes a session type. The Koko-to-TypeScript bridge protocol becomes a session type. Violations are caught by the compiler, not by users reporting broken behavior.

Whether this is practical today in Elixir — probably not yet. The Dialyzer does some of this work but doesn’t model communication protocols. But the theory is sound, the papers exist, and someone already built Par as a real language implementing CP. The question is when, not whether, this reaches production language ecosystems.

The lineage

Session types didn’t appear from nowhere. The intellectual thread:

1987 — Jean-Yves Girard introduces linear logic. Resources, not propositions. Use once.

1993 — Kohei Honda introduces session types. Static checking that concurrent programs follow communication protocols.

1994 — Samson Abramsky explores computational interpretations of linear logic. Bellin and Scott connect π-calculus to linear logic.

1997 — Wadler and Marlow publish “A practical subtyping system for Erlang” — the Erlang and formal methods worlds directly intersect.

2010 — Luís Caires and Frank Pfenning discover a Curry-Howard correspondence between dual intuitionistic linear logic and session-typed π-calculus.

2012 — Wadler’s “Propositions as Sessions” — classical linear logic, the CP/GV calculi, deadlock freedom by construction.

2016 — Multiparty session types: duality (2 types) generalizes to coherence (N types). Real systems have more than two participants.

2019 — Gradual session types: bridge static and dynamic typing for session-typed communication. Crucial for polyglot microservices.

2025 — Par implements CP as a real concurrent language.

What I’m watching for

The Koko experiment (ADR-0115) will produce concrete data on whether BEAM’s runtime model delivers measurable advantages for agent infrastructure. The shadow executor (ADR-0118) gives us apples-to-apples comparison data.

But the Armstrong/Wadler convergence points at something bigger: the possibility of agent systems where communication protocols are proven correct before deployment and runtime failures are automatically recovered — both at the same time, in the same system.

Armstrong built the runtime half. Wadler proved the theory for the other half. Putting them together is still an open research problem. Koko is my small bet that it’s worth exploring.