The stabiliser fragment of quantum theory is a foundational building block for quantum error correction and the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal and complete denotational semantics for stabiliser operations which include measurement and classical control and in which quantum error-correcting codes are first-class objects. The operations are interpreted as certain \emph{affine relations}, offering a significantly simpler alternative to the standard operator-algebraic semantics of quantum programs.

We demonstrate the power of the resulting semantics by describing a small, proof-of-concept assembly language for stabiliser programs with fully-abstract denotational semantics.

Full paper at: https://robertbooth.fr/pdfs/Denotational_semantics_for_stabiliser_quantum_programs.pdf