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

ACM SIGPLAN Notices

Algebraic Effects, Linearity, and Quantum Programming Languages

Sam Staton

Published Jan 14, 2015• 11 citations
Publisher

Abstract

We develop a new framework of algebraic theories with linear parameters, and use it to analyze the equational reasoning principles of quantum computing and quantum programming languages. We use the framework as follows: we present a new elementary algebraic theory of quantum computation, built from unitary gates and measurement; we provide a completeness theorem or the elementary algebraic theory by relating it with a model from operator algebra; we extract an equational theory for a quantum programming language from the algebraic theory; we compare quantum computation with other local notions of computation by investigating variations on the algebraic theory.

DOI
10.1145/2775051.2676999

Related papers

Algebraic Effects, Linearity, and Quantum Programming Languages

Sam Staton

We develop a new framework of algebraic theories with linear parameters, and use it to analyze the equational reasoning principles of quantum computing and quantum programming languages. We use the framework as follows:

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)•Dec 19, 2014•47 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

Semantics for a Quantum Programming Language by Operator Algebras

Kenta Cho

This paper presents a novel semantics for a quantum programming language by operator algebras, which are known to give a formulation for quantum theory that is alternative to the one by Hilbert spaces. We show that the opposite category of the category of W*-algebras and normal completely positive subunital maps is an elementary quantum flow chart category in the sense of Selinger. As a consequence, it gives a denotational semantics for Selinger's first-order functional quantum programming language QPL. The use of operator algebras allows us to accommodate infinite structures and to handle classical and quantum computations in a unified way.

arXiv:1412.8545•Electronic Proceedings in Theoretical Computer Science•Dec 28, 2014•18 citations

Free Quantum Computing

Jacques Carette, Chris Heunen, Robin Kaarsgaard +2 more

Quantum computing improves substantially on known classical algorithms for various important problems, but the nature of the relationship between quantum and classical computing is not yet fully understood. This relationship can be clarified by free models, that add to classical computing just enough physical principles to represent quantum computing and no more. Here we develop an axiomatisation of quantum computing that replaces the standard continuous postulates with a small number of discrete equations, as well as a free model that replaces the standard linear-algebraic model with a category-theoretical one. The axioms and model are based on reversible classical computing, isolate quantum advantage in the ability to take certain well-behaved square roots, and link to various quantum computing hardware platforms. This approach allows combinatorial optimisation, including brute force computer search, to optimise quantum computations. The free model may be interpreted as a programming language for quantum computers, that has the same expressivity and computational universality as the standard model, but additionally allows automated verification and reasoning.

quant-pharXiv:2602.16927•Proceedings of the National Academy of Sciences•Feb 20, 2026•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 measurement calculus

Vincent Danos A, Elham Kashefi, Prakash Panangaden

Measurement-based quantum computation has emerged from the physics community as a new approach to quantum computation where the notion of measurement is the main driving force of computation. This is in contrast with the more traditional circuit model that is based on unitary operations. Among measurement-based quantum computation methods, the recently introduced one-way quantum computer [Raussendorf and Briegel 2001] stands out as fundamental. We develop a rigorous mathematical model underlying the one-way quantum computer and present a concrete syntax and operational semantics for programs, which we call patterns , and an algebra of these patterns derived from a denotational semantics. More importantly, we present a calculus for reasoning locally and compositionally about these patterns. We present a rewrite theory and prove a general standardization theorem which allows all patterns to be put in a semantically equivalent standard form. Standardization has far-reaching consequences: a new physical architecture based on performing all the entanglement in the beginning, parallelization by exposing the dependency structure of measurements and expressiveness theorems. Furthermore we formalize several other measurement-based models, for example, Teleportation, Phase and Pauli models and present compositional embeddings of them into and from the one-way model. This allows us to transfer all the theory we develop for the one-way model to these models. This shows that the framework we have developed has a general impact on measurement-based computation and is not just particular to the one-way quantum computer.

Journal of the ACM•Apr 1, 2007•193 citations
We develop a new framework of algebraic theories with linear parameters, and use it to analyze the equational reasoning principles of quantum computing and quantum programming languages. We use the framework as follows: we present a new elementary algebraic theory of quantum computation, built from unitary gates and measurement; we provide a completeness theorem or the elementary algebraic theory by relating it with a model from operator algebra; we extract an equational theory for a quantum programming language from the algebraic theory; we compare quantum computation with other local notions of computation by investigating variations on the algebraic theory.
This paper presents a novel semantics for a quantum programming language by operator algebras, which are known to give a formulation for quantum theory that is alternative to the one by Hilbert spaces. We show that the opposite category of the category of W*-algebras and normal completely positive subunital maps is an elementary quantum flow chart category in the sense of Selinger. As a consequence, it gives a denotational semantics for Selinger's first-order functional quantum programming language QPL. The use of operator algebras allows us to accommodate infinite structures and to handle classical and quantum computations in a unified way.
Quantum computing improves substantially on known classical algorithms for various important problems, but the nature of the relationship between quantum and classical computing is not yet fully understood. This relationship can be clarified by free models, that add to classical computing just enough physical principles to represent quantum computing and no more. Here we develop an axiomatisation of quantum computing that replaces the standard continuous postulates with a small number of discrete equations, as well as a free model that replaces the standard linear-algebraic model with a category-theoretical one. The axioms and model are based on reversible classical computing, isolate quantum advantage in the ability to take certain well-behaved square roots, and link to various quantum computing hardware platforms. This approach allows combinatorial optimisation, including brute force computer search, to optimise quantum computations. The free model may be interpreted as a programming language for quantum computers, that has the same expressivity and computational universality as the standard model, but additionally allows automated verification and reasoning.
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.
Measurement-based quantum computation has emerged from the physics community as a new approach to quantum computation where the notion of measurement is the main driving force of computation. This is in contrast with the more traditional circuit model that is based on unitary operations. Among measurement-based quantum computation methods, the recently introduced one-way quantum computer [Raussendorf and Briegel 2001] stands out as fundamental. We develop a rigorous mathematical model underlying the one-way quantum computer and present a concrete syntax and operational semantics for programs, which we call patterns , and an algebra of these patterns derived from a denotational semantics. More importantly, we present a calculus for reasoning locally and compositionally about these patterns. We present a rewrite theory and prove a general standardization theorem which allows all patterns to be put in a semantically equivalent standard form. Standardization has far-reaching consequences: a new physical architecture based on performing all the entanglement in the beginning, parallelization by exposing the dependency structure of measurements and expressiveness theorems. Furthermore we formalize several other measurement-based models, for example, Teleportation, Phase and Pauli models and present compositional embeddings of them into and from the one-way model. This allows us to transfer all the theory we develop for the one-way model to these models. This shows that the framework we have developed has a general impact on measurement-based computation and is not just particular to the one-way quantum computer.