Paper 6 - Executable Causal Diagrams with Typed Linear Frontiers

Landing page for the Executable Causal Diagrams with Typed Linear Frontiers draft. Abstract, status, figures, and related material for the frontier-transformer causal pipeline framing.

Updated

On this page
  1. Status
  2. Abstract
  3. Figures
  4. Related

Paper 6 - Executable Causal Diagrams with Typed Linear Frontiers

This draft frames Wire as executable causal diagram syntax: <> forms incomparable frontiers, => consumes compatible endpoint pairs while carrying unmatched endpoints forward, and named typed ports determine which observations may cross the composed boundary. Typed linear frontiers provide the accounting discipline for that diagram.

Status

Draft manuscript. See manuscript.md for the Markdown text and typst/manuscript.typ for the submission-ready PDF source registered as a Nix docs output. The PDF uses the shared profile-driven Cortex submission template under docs/Publications/_typst/.

Public artifact context is available through the Cortex documentation and the proof-status dashboard, the live source of truth for current Lean mechanization and Haskell correspondence.

Abstract

Wire is a source language for executable causal diagrams. Its surface is a typed frontier-transformer calculus: <> forms incomparable frontier union, => consumes compatible endpoint pairs and carries unmatched endpoints forward, and typed ports decide which observations may cross the composed boundary. The draft uses an async dashboard diamond as its canonical example: fetch a user, derive distinct branch facts in CorePure (Wire’s deterministic expression layer), fetch posts and friends independently, carry the profile fact directly to the join, then assemble the response. In host languages the diamond is a property of execution; in Wire the admitted diagram is the shared object. The Cortex artifact aligns algebraic graph syntax, source elaboration, circuit lowering to Pulse, Cortex’s durable runtime, proof-track admission slices, and a Lean-facing post-elaboration IR. The public proof-status dashboard links the relevant Lean declarations and distinguishes proven claims, runtime hooks, tests, witnesses, and remaining correspondence obligations.

Figures