2026-07-20T14:42:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26358 2026-07-15T06:01:56Z ddc:004 open_access

Denotational Semantics for Stabiliser Quantum Programs Booth, Robert I. Comfort, Cole quantum programming languages quantum error correction denotational semantics categorical semantics stabiliser theory symplectic linear algebra 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robert I. Booth and Cole Comfort 2026 Is Part Of LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2026.8 urn:nbn:de:0030-drops-263580 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.8 eng https://creativecommons.org/licenses/by/4.0/legalcode