DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.7

Graphical Symplectic Algebra

Authors: Robert I. Booth, Titouan Carette, and Cole Comfort

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

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.

Cite as

Robert I. Booth, Titouan Carette, and Cole Comfort. Graphical Symplectic Algebra. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{booth_et_al:LIPIcs.FSCD.2026.7,
  author =	{Booth, Robert I. and Carette, Titouan and Comfort, Cole},
  title =	{{Graphical Symplectic Algebra}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{7:1--7:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.7},
  URN =		{urn:nbn:de:0030-drops-263573},
  doi =		{10.4230/LIPIcs.FSCD.2026.7},
  annote =	{Keywords: graphical algebra, symplectic geometry, string diagrams, category theory, classical mechanics, quantum mechanics, graph theory}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2026.8

Denotational Semantics for Stabiliser Quantum Programs

Authors: Robert I. Booth and Cole Comfort

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

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.

Cite as

Robert I. Booth and Cole Comfort. Denotational Semantics for Stabiliser Quantum Programs. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{booth_et_al:LIPIcs.FSCD.2026.8,
  author =	{Booth, Robert I. and Comfort, Cole},
  title =	{{Denotational Semantics for Stabiliser Quantum Programs}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{8:1--8:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.8},
  URN =		{urn:nbn:de:0030-drops-263580},
  doi =		{10.4230/LIPIcs.FSCD.2026.8},
  annote =	{Keywords: quantum programming languages, quantum error correction, denotational semantics, categorical semantics, stabiliser theory, symplectic linear algebra}
}

Search Results

Documents authored by Comfort, Cole

Graphical Symplectic Algebra

Abstract

Cite as

Denotational Semantics for Stabiliser Quantum Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message