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}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2022.24

Complete ZX-Calculi for the Stabiliser Fragment in Odd Prime Dimensions

Authors: Robert I. Booth and Titouan Carette

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract

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.

Cite as

Robert I. Booth and Titouan Carette. Complete ZX-Calculi for the Stabiliser Fragment in Odd Prime Dimensions. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{booth_et_al:LIPIcs.MFCS.2022.24,
  author =	{Booth, Robert I. and Carette, Titouan},
  title =	{{Complete ZX-Calculi for the Stabiliser Fragment in Odd Prime Dimensions}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.24},
  URN =		{urn:nbn:de:0030-drops-168225},
  doi =		{10.4230/LIPIcs.MFCS.2022.24},
  annote =	{Keywords: ZX-calculus, completeness, quantum, stabiliser, qudits}
}

Search Results

Documents authored by Booth, Robert I.

Graphical Symplectic Algebra

Abstract

Cite as

Denotational Semantics for Stabiliser Quantum Programs

Abstract

Cite as

Complete ZX-Calculi for the Stabiliser Fragment in Odd Prime Dimensions

Abstract

Cite as

Thanks for your feedback!

Could not send message