Causality and Semantic Separation: Artifact

This artifact accompanies the paper Causality and Semantic Separation, accepted to PLDI 2026. The full version of the paper, including appendices, is on arXiv. It contains a mechanized formalization of causal models in the Rocq Prover, together with a proof of the paper's main result: that semantic separation is equivalent to d-separation, the standard graphical independence criterion used in causal inference. The artifact includes: Formal definitions of causal graphs, assignments, and function-based semantics A mechanized definition of semantic separation A Rocq proof of equivalence between semantic separation and d-separation The repository is designed to be built using Docker. See README.md for instructions on building the artifact.