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

arXiv:2509.04527

The Structure and Interpretation of Quantum Programs I: Foundations

David Wakeham

Published Sep 3, 2025• 0 citations
arXivHTMLPDF

Abstract

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.

DOI
10.48550/arxiv.2509.04527

Related papers

Algebraic and Mathematical Foundations of Quantum Computation: Hilbert Spaces, Group Structures, and Quantum Algorithms

Bhavesh B. Prajapati

Quantum computation is, at bottom, a branch of applied algebra and functional analysis: the state of a quantum register is a unit vector in a finite-dimensional complex Hilbert space, computation is the action of the unitary group on that space, and the structure of the most important quantum algorithms is dictated by the representation theory of finite and continuous groups. This paper develops the mathematical scaffolding of the field from first principles and uses it to explain why quantum computers can outperform classical ones. We review complex inner-product spaces, self-adjoint and unitary operators, the spectral theorem, and the tensor-product construction that gives rise to entanglement and the exponential dimension of the state space. We then describe the qubit and its geometry, the group-theoretic classification of quantum gates (the special unitary groups, the Pauli and Clifford groups, and their Lie-algebraic generators), and the universality results that justify finite gate sets together with the Solovay–Kitaev theorem. With this apparatus we analyse the quantum Fourier transform, phase estimation, and the hidden subgroup problem, showing how Shor’s factoring algorithm, Grover’s search, and the quantum linear-systems algorithm arise as instances of a small number of algebraic templates. Finally we treat the stabilizer formalism of quantum error correction—where finite abelian groups over GF(2) play the central role—and the variational, near-term (NISQ) algorithms that dominate current practice. Throughout, the emphasis is on the algebraic invariants that make quantum speed-ups possible.

Communications on Applied Nonlinear Analysis•Jan 24, 2025•0 citations

Quantum Computing Preliminaries: The Mathematical Language of Quantum Computing

P. K. Majumdar

Quantum computing uses a mathematical language that can seem unfamiliar to readers from programming, engineering and other technical backgrounds. Qubits are represented by vectors, quantum gates by matrices, measurement outcomes by eigenvalues, and probability amplitudes by complex numbers. Quantum Computing Preliminaries develops this language carefully, connecting each mathematical idea with its computational and physical meaning. The book begins with complex vector spaces and explains why quantum states require more than classical probabilities. It introduces qubits, superposition, normalisation, basis vectors and Dirac bra–ket notation, supported by worked calculations and geometric interpretation using the Bloch sphere. The discussion then turns to inner products and the geometry of quantum states. Readers learn how to calculate norms, test orthogonality, determine state overlap and apply the Born rule. Particular attention is given to complex conjugation and the distinction between the ordinary dot product and the Hermitian inner product used in quantum mechanics.The treatment of matrix operators establishes the roles of linear, unitary and Hermitian operators. It explains matrix multiplication, non-commutativity, eigenvalues, eigenvectors, reversibility and norm preservation. The Pauli and Hadamard gates provide concrete examples that link matrix algebra to rotations, the Bloch sphere, quantum-state evolution, and measurement. Outer products and projection operators are developed as tools for constructing operators, selecting state components and describing ideal projective measurements. The book examines idempotence, completeness, repeated measurement and the distinction between the ket–bra outer product and the tensor product used to form composite quantum systems. The final chapter explores changes of basis, operator representations and diagonalisation. It shows how the same physical state or operation can have different numerical representations in the computational and Hadamard bases. Readers derive the similarity transformation, use outer-product substitution, diagonalise Hermitian operators and interpret the spectral decomposition geometrically. Examples involving the Pauli-X, Pauli-Y, Pauli-Z and Hadamard operators demonstrate how basis choice exposes phase, population and measurement structure without changing the underlying physics. Throughout the book, Python and NumPy examples translate the mathematics into executable calculations. The programs demonstrate complex-vector operations, inner products, eigendecomposition, basis transformation and numerical verification while explaining the importance of using operations suited to complex Hilbert spaces. Each chapter includes conceptual, mathematical, computational and challenge exercises. Detailed solutions provide step-by-step derivations, program output and physical interpretation, allowing the book to support both guided study and independent practice. Quantum Computing Preliminaries is intended for students, software developers, engineers and technically minded readers preparing to study quantum circuits, algorithms, simulation, measurement, entanglement or error correction. It assumes familiarity with elementary algebra and programming but does not require prior training in quantum mechanics. Its purpose is to provide a clear mathematical foundation for understanding how quantum information is represented, transformed and measured.

•Sep 4, 2026•0 citations

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

Logical Structures Underlying Quantum Computing

Federico Holik, Giuseppe Sergioli, Hector Freytes +1 more

In this work we advance a generalization of quantum computational logics capable of dealing with some important examples of quantum algorithms. We outline an algebraic axiomatization of these structures.

arXiv:1811.06808•Entropy•Jan 16, 2019•6 citations

Combiner le contrôle classique et quantique : une perspective logique, syntaxique et sémantique

Kinnari Vijay Dave

The focus of this thesis is on laying the theoretical foundation for designing an all-encompassing programming language for quantum computing. The idea inspiring all the contributions of this thesis was to mirror the development of programming languages and logic done for classical computing for its quantum counterpart. Following the groundwork of the Curry-Howard-Lambek correspondence, we try to delve into the three cornerstones of this correspondence - programming languages, logic and category theory with a focus on combining two paradigms of control flow in programs - quantum and classical into one framework. We have tried to achieve more. We have also touched upon the two complementary view of quantum mechanics- Heisenberg and Schrödinger, and adopted one view to define a physically intuitive semantics for the languages we discuss. There are two main contributions that this thesis makes to the existing literature on quantum programming languages. We first introduce a quantum lambda calculus which combines quantum and classical control, whose design is guided by the mathematical structure of its physically intuitive denotational semantics. The operational semantics for this language, is based on an adaptation of quantum configurations which we introduce, and is tied to the denotational model through an adequacy result. The language also provides a prototype of quantum inductive types through the type qnat- a type for quantum natural numbers. The denotational model for this calculus is based on von Neumann algebras- which are at the heart of the mathematical formulation of the Heisenberg view of quantum mechanics. The second contribution is a proof language for the IMALL fragment of Linear logic which builds on some key observations from the calculus introduced above. This language is one of the first such works to be able to support programs which combine constructs such as the quantum switch with measurement. In this aspect, this work is a strict improvement on the previous calculus, since it supports a more fine grained version of quantum control, thus enabling expression of algorithms such as the well-known quantum switch. The syntax is also linear algebraic in nature, supporting linear combinations of terms. A key consequence of this, along with the semantics of the B modality that it introduces is that measurement is no longer a ground construct of the language. In fact, it can now be written as just another program in the language. Finally, the denotational semantics for this work is based on C*-algebras - a generalization of von Neumann algebras. The denotational model is shown to be adequate for the operational semantics, whose linearity turns out to be a natural consequence of this. Finally, we conclude this thesis with limitations of these works and possible directions for future work.

•Dec 17, 2025•0 citations

Logical structures underlying quantum computing

Federico Holik, Giuseppe Sergioli, Héctor Freytes +1 more

In this work we advance a generalization of quantum computational logics capable of dealing with some important examples of quantum algorithms. We outline an algebraic axiomatization of these structures.

•Jan 1, 2019•6 citations
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 computation is, at bottom, a branch of applied algebra and functional analysis: the state of a quantum register is a unit vector in a finite-dimensional complex Hilbert space, computation is the action of the unitary group on that space, and the structure of the most important quantum algorithms is dictated by the representation theory of finite and continuous groups. This paper develops the mathematical scaffolding of the field from first principles and uses it to explain why quantum computers can outperform classical ones. We review complex inner-product spaces, self-adjoint and unitary operators, the spectral theorem, and the tensor-product construction that gives rise to entanglement and the exponential dimension of the state space. We then describe the qubit and its geometry, the group-theoretic classification of quantum gates (the special unitary groups, the Pauli and Clifford groups, and their Lie-algebraic generators), and the universality results that justify finite gate sets together with the Solovay–Kitaev theorem. With this apparatus we analyse the quantum Fourier transform, phase estimation, and the hidden subgroup problem, showing how Shor’s factoring algorithm, Grover’s search, and the quantum linear-systems algorithm arise as instances of a small number of algebraic templates. Finally we treat the stabilizer formalism of quantum error correction—where finite abelian groups over GF(2) play the central role—and the variational, near-term (NISQ) algorithms that dominate current practice. Throughout, the emphasis is on the algebraic invariants that make quantum speed-ups possible.
Quantum computing uses a mathematical language that can seem unfamiliar to readers from programming, engineering and other technical backgrounds. Qubits are represented by vectors, quantum gates by matrices, measurement outcomes by eigenvalues, and probability amplitudes by complex numbers. Quantum Computing Preliminaries develops this language carefully, connecting each mathematical idea with its computational and physical meaning. The book begins with complex vector spaces and explains why quantum states require more than classical probabilities. It introduces qubits, superposition, normalisation, basis vectors and Dirac bra–ket notation, supported by worked calculations and geometric interpretation using the Bloch sphere. The discussion then turns to inner products and the geometry of quantum states. Readers learn how to calculate norms, test orthogonality, determine state overlap and apply the Born rule. Particular attention is given to complex conjugation and the distinction between the ordinary dot product and the Hermitian inner product used in quantum mechanics.The treatment of matrix operators establishes the roles of linear, unitary and Hermitian operators. It explains matrix multiplication, non-commutativity, eigenvalues, eigenvectors, reversibility and norm preservation. The Pauli and Hadamard gates provide concrete examples that link matrix algebra to rotations, the Bloch sphere, quantum-state evolution, and measurement. Outer products and projection operators are developed as tools for constructing operators, selecting state components and describing ideal projective measurements. The book examines idempotence, completeness, repeated measurement and the distinction between the ket–bra outer product and the tensor product used to form composite quantum systems. The final chapter explores changes of basis, operator representations and diagonalisation. It shows how the same physical state or operation can have different numerical representations in the computational and Hadamard bases. Readers derive the similarity transformation, use outer-product substitution, diagonalise Hermitian operators and interpret the spectral decomposition geometrically. Examples involving the Pauli-X, Pauli-Y, Pauli-Z and Hadamard operators demonstrate how basis choice exposes phase, population and measurement structure without changing the underlying physics. Throughout the book, Python and NumPy examples translate the mathematics into executable calculations. The programs demonstrate complex-vector operations, inner products, eigendecomposition, basis transformation and numerical verification while explaining the importance of using operations suited to complex Hilbert spaces. Each chapter includes conceptual, mathematical, computational and challenge exercises. Detailed solutions provide step-by-step derivations, program output and physical interpretation, allowing the book to support both guided study and independent practice. Quantum Computing Preliminaries is intended for students, software developers, engineers and technically minded readers preparing to study quantum circuits, algorithms, simulation, measurement, entanglement or error correction. It assumes familiarity with elementary algebra and programming but does not require prior training in quantum mechanics. Its purpose is to provide a clear mathematical foundation for understanding how quantum information is represented, transformed and measured.
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.
The focus of this thesis is on laying the theoretical foundation for designing an all-encompassing programming language for quantum computing. The idea inspiring all the contributions of this thesis was to mirror the development of programming languages and logic done for classical computing for its quantum counterpart. Following the groundwork of the Curry-Howard-Lambek correspondence, we try to delve into the three cornerstones of this correspondence - programming languages, logic and category theory with a focus on combining two paradigms of control flow in programs - quantum and classical into one framework. We have tried to achieve more. We have also touched upon the two complementary view of quantum mechanics- Heisenberg and Schrödinger, and adopted one view to define a physically intuitive semantics for the languages we discuss. There are two main contributions that this thesis makes to the existing literature on quantum programming languages. We first introduce a quantum lambda calculus which combines quantum and classical control, whose design is guided by the mathematical structure of its physically intuitive denotational semantics. The operational semantics for this language, is based on an adaptation of quantum configurations which we introduce, and is tied to the denotational model through an adequacy result. The language also provides a prototype of quantum inductive types through the type qnat- a type for quantum natural numbers. The denotational model for this calculus is based on von Neumann algebras- which are at the heart of the mathematical formulation of the Heisenberg view of quantum mechanics. The second contribution is a proof language for the IMALL fragment of Linear logic which builds on some key observations from the calculus introduced above. This language is one of the first such works to be able to support programs which combine constructs such as the quantum switch with measurement. In this aspect, this work is a strict improvement on the previous calculus, since it supports a more fine grained version of quantum control, thus enabling expression of algorithms such as the well-known quantum switch. The syntax is also linear algebraic in nature, supporting linear combinations of terms. A key consequence of this, along with the semantics of the B modality that it introduces is that measurement is no longer a ground construct of the language. In fact, it can now be written as just another program in the language. Finally, the denotational semantics for this work is based on C*-algebras - a generalization of von Neumann algebras. The denotational model is shown to be adequate for the operational semantics, whose linearity turns out to be a natural consequence of this. Finally, we conclude this thesis with limitations of these works and possible directions for future work.