The stabiliser fragment of quantum theory is a foundational building block for quantum error correction, and hence for the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal, and complete denotational semantics for stabiliser operations, including measurement, classically controlled Pauli operators, and affine classical computation, thereby supporting an explicit treatment of quantum error-correcting codes. We interpret stabiliser operations as affine relations over finite fields, yielding a semantics that reflects the algebraic structure underlying stabiliser quantum error correction. Because stabiliser quantum mechanics has a well-behaved algebraic structure, our relational semantics is conceptually transparent and computationally tractable when compared to standard denotational models for general quantum programs. We demonstrate the resulting semantics by describing a small, low-level assembly language for stabiliser programs with fully abstract denotational semantics.

We introduce a family of diagrammatical equational theories unifying two research programs: categorical quantum mechanics and graphical linear algebra. We prove their completeness with respect to denotational semantics described in terms of relations between vector spaces equipped with symplectic structure. This provides versatile graphical languages encompassing both affinely constrained classical mechanical systems, as well as odd-prime-dimensional stabiliser and Gaussian quantum circuits. Terms are described by labelled graphs with input and output interfaces, and the languages are equipped with equational theories amenable to standard graph rewriting techniques. In order to reason about large composite systems, we introduce a compact scalable notation where the vertices are themselves labelled by graphs. This notation allows us to state new and powerful rewrite rules which operate on diagrams at a large scale. We also show how this notation neatly captures some important constructions, such as graph states of quantum computing and the impedance and admittance matrices of electrical networks.

We introduce a family of ZX-calculi which axiomatise the stabiliser fragment of quantum theory in odd prime dimensions. These calculi recover many of the nice features of the qubit ZX-calculus which were lost in previous proposals for higher-dimensional systems. We then prove that these calculi are complete, i.e. provide a set of rewrite rules which can be used to prove any equality of stabiliser quantum operations. Adding a discard construction, we obtain a calculus complete for mixed state stabiliser quantum mechanics in odd prime dimensions, and this furthermore gives a complete axiomatisation for the related diagrammatic language for affine co-isotropic relations.