Inductive diagrams for causal reasoning
summary
Defines causal separation diagrams as an inductive, diagrammatic syntax that makes impossible executions unrepresentable and enforces consistent cuts, then gives three semantic interpreters: proof-relevant causal paths, parametric clock functions, and clock-condition proofs. Implements the whole framework mechanized in Agda with source on GitHub and produces a generic proof of Lamport's clock condition instantiated on Lamport scalar, Mattern vector, and two matrix clocks (Raynal et al., Wuu & Bernstein), yielding verified clock implementations.
AI-written summary · about
chapters (10)
- 0:00Inductive diagrams intro
- 1:22Traditional model limits
- 3:54Introducing causal separation diagrams
- 5:43Departure from models
- 8:11Prioritizing causal boundaries
- 10:19Graph syntax and rules
- 12:48Composition rules
- 13:54Semantic interpretations of CSDs
- 15:38Future directions
- 16:03Q&A
related talks
18mDistributed Causal Memory for Higher-Order Distributed Separation Logic
19mCausality and Semantic Separation
28mReasoning about Distributed Reconfigurable Systems
33mCausality is simple #bbuzz
22mA Calculus of Inductive Linear Constructions
17mCalculational design of Incorrectness Separation Logic
49mFrom ZX to first order logic: a survey of string diagrammatic calculi
24mSymbolic Execution with Separating Decision Diagrams