Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Leibniz international proceedings in informatics

Denotational Semantics for Stabiliser Quantum Programs

Robert I. Booth, Cole Comfort

Published Jan 1, 2026• 0 citations
Publisher

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.

DOI
10.4230/lipics.fscd.2026.8

Related papers

Denotational semantics for stabiliser quantum programs

Robert I. Booth, Cole Comfort

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, classically-controlled Pauli operators, and affine classical operations, in which quantum error-correcting codes are first-class objects. The operations are interpreted as certain affine relations over finite fields. This offers a conceptually motivated and computationally-tractable alternative to the standard operator-algebraic semantics of quantum programs (whose time complexity grows exponentially as the state space increases in size). 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.

cs.LOCross-listedarXiv:2511.22734•Dec 1, 2025•0 citations

The Structure and Interpretation of Quantum Programs I: Foundations

David Wakeham

Qubits are a great way to build a quantum computer, but a limited way to program one. We replace the usual "states and gates" formalism with a "props and ops" (propositions and operators) model in which (a) the C*-algebra of observables supplies the syntax; (b) states, viewed as linear functionals, give the semantics; and (c) a novel diagrammatic calculus unifies the two. The first part develops the basic objects of the framework, encoding consistent patterns of operator correlation, recovering Hilbert space via the GNS construction, and re-deriving the Bloch sphere as the set of all consistent correlations of operators in the Pauli algebra. We then turn to intervention, showing how measurement modifies state, proving an operator-algebraic version of the Knill-Laflamme conditions, and expressing stabilizer codes with the same diagrammatic machinery. This provides a concise, representation-agnostic account of quantum error correction. The result is a self-contained foundation in which C*-algebras, and their dual Hilbert spaces, offer a rich and universal substrate for quantum programming; forthcoming papers will build a high-level language and quantum software applications on top of this substrate.

arXiv:2509.04527•Sep 3, 2025•0 citations

The XP Stabilizer Formalism

Mark Webster

Quantum computers are expected to have advantages over classical computers in solving a range of high impact problems, but they are highly susceptible to errors due to environmental noise. The Pauli Stabiliser formalism generalises classical error-correction methods and makes use of quantum error correction codes to protect quantum information. In this thesis, we introduce the XP stabiliser formalism, which is a generalisation of the Pauli stabiliser formalism with a number of useful applications. Quantum algorithms are typically written in terms of quantum circuits which involve a series of unitary gates followed by measurements which form the output of the computation. To implement quantum algorithms reliably, we need to perform unitary gates fault-tolerantly so that errors do not propagate in an uncontrolled way. Transversal logical operators are one way of applying unitary gates fault-tolerantly on Pauli stabiliser codes. Identifying transversal logical operators for a given Pauli stabiliser code is challenging, and existing methods have exponential complexity in one or more of the parameters of the code. Making use of the XP formalism, we present efficient algorithms which identify all transversal logical operators that are diagonal in the computational basis for any Pauli stabiliser code. We also show how to construct codes with a transversal implementation of any desired diagonal logical operator. The Pauli stabiliser formalism can also be used to efficiently represent certain quantum states, but many states of interest lie outside the formalism. In the XP formalism, a wider range of states can be represented than in the Pauli stabiliser formalism, including hypergraph states which have interesting non-local properties. The braiding of non-Abelian anyons is a proposed pathway to universal fault-tolerant quantum computation. Certain XP stabiliser codes are known to harbour non-Abelian anyons, and can be studied within the new formalism.

•Jan 1, 2023•0 citations

Quantum Control and General Recursion Beyond the Unitary Case

Kathleen Barsse, Romain Péchoux, Simon Perdrix

Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.

arXiv:2507.10466•Leibniz international proceedings in informatics•Jul 14, 2025•0 citations

Semantics for variational Quantum programming

Xiaodong Jia, Andre Kornell, Bert Lindenhovius +2 more

We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.

arXiv:2107.13347•Proceedings of the ACM on Programming Languages•Jan 12, 2022•16 citations

An Algebra of Pure Quantum Programming

Thorsten Altenkirch, Jonathan Grattage, Juliana Kaizer Vizzotto +1 more

We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously developed denotational semantics of QML. The completeness proof also gives rise to a normalisation algorithm following the normalisation-by-evaluation approach. The current work focuses on the pure fragment of QML, omitting measurements.

arXiv:quant-ph/0506012•Electronic Notes in Theoretical Computer Science•Mar 1, 2007•37 citations
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.
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, classically-controlled Pauli operators, and affine classical operations, in which quantum error-correcting codes are first-class objects. The operations are interpreted as certain affine relations over finite fields. This offers a conceptually motivated and computationally-tractable alternative to the standard operator-algebraic semantics of quantum programs (whose time complexity grows exponentially as the state space increases in size). 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.
Qubits are a great way to build a quantum computer, but a limited way to program one. We replace the usual "states and gates" formalism with a "props and ops" (propositions and operators) model in which (a) the C*-algebra of observables supplies the syntax; (b) states, viewed as linear functionals, give the semantics; and (c) a novel diagrammatic calculus unifies the two. The first part develops the basic objects of the framework, encoding consistent patterns of operator correlation, recovering Hilbert space via the GNS construction, and re-deriving the Bloch sphere as the set of all consistent correlations of operators in the Pauli algebra. We then turn to intervention, showing how measurement modifies state, proving an operator-algebraic version of the Knill-Laflamme conditions, and expressing stabilizer codes with the same diagrammatic machinery. This provides a concise, representation-agnostic account of quantum error correction. The result is a self-contained foundation in which C*-algebras, and their dual Hilbert spaces, offer a rich and universal substrate for quantum programming; forthcoming papers will build a high-level language and quantum software applications on top of this substrate.
Quantum computers are expected to have advantages over classical computers in solving a range of high impact problems, but they are highly susceptible to errors due to environmental noise. The Pauli Stabiliser formalism generalises classical error-correction methods and makes use of quantum error correction codes to protect quantum information. In this thesis, we introduce the XP stabiliser formalism, which is a generalisation of the Pauli stabiliser formalism with a number of useful applications. Quantum algorithms are typically written in terms of quantum circuits which involve a series of unitary gates followed by measurements which form the output of the computation. To implement quantum algorithms reliably, we need to perform unitary gates fault-tolerantly so that errors do not propagate in an uncontrolled way. Transversal logical operators are one way of applying unitary gates fault-tolerantly on Pauli stabiliser codes. Identifying transversal logical operators for a given Pauli stabiliser code is challenging, and existing methods have exponential complexity in one or more of the parameters of the code. Making use of the XP formalism, we present efficient algorithms which identify all transversal logical operators that are diagonal in the computational basis for any Pauli stabiliser code. We also show how to construct codes with a transversal implementation of any desired diagonal logical operator. The Pauli stabiliser formalism can also be used to efficiently represent certain quantum states, but many states of interest lie outside the formalism. In the XP formalism, a wider range of states can be represented than in the Pauli stabiliser formalism, including hypergraph states which have interesting non-local properties. The braiding of non-Abelian anyons is a proposed pathway to universal fault-tolerant quantum computation. Certain XP stabiliser codes are known to harbour non-Abelian anyons, and can be studied within the new formalism.
Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.
We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.