  The Lamport diagram is a pervasive and intuitive tool for informal reasoning
about "happens-before" relationships in a concurrent system. However,
traditional axiomatic formalizations of Lamport diagrams can be painful to work
with in a mechanized setting like Agda. We propose an alternative, inductive
formalization -- the causal separation diagram (CSD) -- that takes inspiration
from string diagrams and concurrent separation logic, but enjoys a graphical
syntax similar to Lamport diagrams. Critically, CSDs are based on the idea that
causal relationships between events are witnessed by the paths that information
follows between them. To that end, we model happens-before as a dependent type
of paths between events.
  The inductive formulation of CSDs enables their interpretation into a variety
of semantic domains. We demonstrate the interpretability of CSDs with a case
study on properties of logical clocks, widely-used mechanisms for reifying
causal relationships as data. We carry out this study by implementing a series
of interpreters for CSDs, culminating in a generic proof of Lamport's clock
condition that is parametric in a choice of clock. We instantiate this proof on
Lamport's scalar clock, on Mattern's vector clock, and on the matrix clocks of
Raynal et al. and of Wuu and Bernstein, yielding verified implementations of
each. The CSD formalism and our case study are mechanized in the Agda proof
assistant.
