Searcharxiv⌕ Search

arXiv subjects

Chris Heunen

Publications and source records attributed to Chris Heunen.

At least 19 recordsLinked to original sources
arXiv2026

A Dynamic Intermediate Representation for Hybrid Quantum-Classical Programs

Quantum compilers typically follow the circuit model, representing programs as fixed sequences of gates. This static view breaks down in hybrid quantum-classical applications, where gate choices depend on runtime data or measurement results. We introduce a new Intermediate Representation (IR) that elevates gates to first-class values, enabling their dynamic creation, composition, and control. This unified representation allows classical computation to steer quantum behaviour, capturing phenomena including stochastic gate selection, adaptive error correction, and measurement-driven computation within a single framework. Case studies in noise modelling, randomised compilation, error correction, and measurement-based quantum computing show that our IR expresses these programs compactly and supports optimisations that were not possible in the circuit model. Evaluation on a benchmark suite of hybrid quantum-classical programs indicates that our IR represents programs compactly and facilitates compiler analysis and transformation.

cs.PL↗
arXiv2026

Hilbert $*$-categories: Where limits in analysis and category theory meet

This article introduces Hilbert $*$-categories: an abstraction of categories having algebraic and analytic properties similar to those of the categories of real, complex, and quaternionic Hilbert spaces and bounded linear maps. Other examples include categories of Hilbert W*-modules and of unitary representations of groupoids. Hilbert $*$-categories are "analytically" complete in two ways: every bounded increasing sequence of Hermitian endomorphisms has a supremum, and every suitably bounded orthogonal family of parallel morphisms is summable. These "analytic" completeness properties are not assumed outright; rather, they are derived, respectively, from two new universal constructions: codirected $\ell^2$-limits of contractions and $\ell^2$-products. In turn, these are built from directed colimits in the wide subcategory of isometries.

math.CT↗
arXiv2026

Unitary Synthesis with Near-Optimal T-Count for Near-Clifford Unitaries

We present an approach to unitary synthesis that implements an arbitrary $n$-qubit unitary operator $U$ by a Clifford+T circuit with T-count $\widetilde{O}(2^n d_F^{\mathcal{C}}(U))$, where $d_F^{\mathcal{C}}(U)$ is the Frobenius norm distance of $U$ to the Clifford group. The T-count is shown to be near-optimal when $d_F^{\mathcal{C}}(U)$ is a constant. Our approach improves the previous best upper bound $\widetilde{O}(2^{4n/3})$ due to Tan (2025) for a large class of unitary operators $U$ as long as $d_F^{\mathcal{C}}(U) \ll 2^{n/3}$.

quant-ph↗
arXiv2026

One rig to control them all

Controlled commands -- computations whose execution depends on a separate input -- play a central role in reversible Boolean circuits and quantum circuits. However, existing formalisms typically treat control only implicitly, entangled with other aspects of computation. From a semantic perspective, control is most naturally expressed in semisimple rig categories, which -- unlike standard circuit models such as props -- support both parallel and conditional composition. We present a construction that freely adjoins an explicit syntactic notion of control to a circuit theory specified as a suitable prop, subject to eight universally quantified equations. Our main result is that these equations are sound and complete for the intended semantics of control: the resulting theory satisfies a universal property, identifying it exactly as the circuit subtheory of the free semisimple rig completion. The proof combines coherence for rig categories with a new method based on induction over Gray codes. We illustrate the usefulness of the framework by showing that it simplifies several existing sound and complete axiomatisations of quantum circuits, isolating a small and conceptually clean set of generators and equations. In addition, the same equations yield a sound and complete axiomatisation of the multiply controlled Toffoli gate set, that is universal for reversible Boolean circuits.

cs.LO↗
arXiv2026

Free Quantum Computing

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-ph↗
arXiv2025

Quantum Circuits Are Just a Phase

Quantum programs today are written at a low level of abstraction - quantum circuits akin to assembly languages - and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed. To this end, we introduce a simple syntax for generating unitaries from "just a phase"; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the "if let" construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design. We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover's search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.

cs.PL↗
arXiv2025

Hadamard-Pi: Equational Quantum Programming

Quantum computing offers advantages over classical computation, yet the precise features that set the two apart remain unclear. In the standard quantum circuit model, adding a 1-qubit basis-changing gate -- commonly chosen to be the Hadamard gate -- to a universal set of classical reversible gates yields computationally universal quantum computation. However, the computational behaviours enabled by this addition are not fully characterised. We give such a characterisation by introducing a small quantum programming language extending the universal classical reversible programming language $Π$ with a single primitive corresponding to the Hadamard gate. The language comes equipped with a sound and complete categorical semantics that is specified by a purely equational theory. Completeness is shown by means of a novel finite presentation, and a corresponding synthesis algorithm, for the groups of orthogonal matrices with entries in the ring $\mathbb{Z}[\tfrac{1}{\sqrt{2}}]$.

quant-ph↗
arXiv2025

Dagger categories of relations: The equivalence of dilatory dagger categories and epi-regular independence categories

Several categories look like categories of relations, but do not fit the established theory of relations in regular categories. They include the category of surjective multivalued functions, the category of injective partial functions, the category of finite probability spaces and stochastic matrices, and the category of Hilbert spaces and linear contractions. To explain these anomalous examples, we develop a parallel theory of relations in epi-regular independence categories. Just as regular categories correspond to tabular allegories, epi-regular independence categories correspond to dilatory dagger categories. The equivalence maps epi-regular independence categories to their associated dagger category of relations, and dilatory dagger categories to their wide subcategory of coisometries.

math.CT↗
arXiv2025

Dagger categories and the complex numbers: Axioms for the category of finite-dimensional Hilbert spaces and linear contractions

We unravel a deep connection between limits of real numbers and limits in category theory. Using a new variant of the classical characterisation of the real numbers, we characterise the category of finite-dimensional Hilbert spaces and linear contractions in terms of simple category-theoretic structures and properties that do not refer to norms, continuity, or real numbers. This builds on Heunen, Kornell, and Van der Schaaf's easier characterisation of the category of all Hilbert spaces and linear contractions.

math.CT↗
arXiv2025

Causal Coverage in Ordered Locales and Spacetimes

We develop relativistic causality theory in the setting of point-free topology by introducing a notion of causal coverage in ordered locales, generalising their canonical coverage relation to incorporate causal structure. This improves Christensen and Crane's construction of `causal sites'. We connect to sheaf theory by showing that causal coverages can be interpreted as a generalised Grothendieck topology, and the sheaf condition as a type of deterministic time evolution. To develop these notions, we introduce and study parallel ordered locales. Causal coverage naturally induces a notion of domain of dependence. Comparing the localic and curve-wise definitions in spacetimes, the localic domains strictly contain the classical ones.

math-ph↗
arXiv2025

String Diagrams for Defect-Based Surface Code Computing

Surface codes are a popular choice for implementing fault-tolerant quantum computing. Two-qubit gates may be realised in these codes using only nearest-neighbour interactions, either by lattice surgery or by braiding defects around each other. The effect of lattice surgery operations may be simply described using the ZX-calculus: a graphical language that has proven effective for program design and optimisation. In this work, we formalise a similar description via the ZX-calculus of defect braiding, as it is conventionally described. We define a graphical calculus KNOT, denoting the logical effects (in the absence of byproduct operations) of defect braiding in surface codes: we show how these effects may be described via a fragment of ZX-calculus which we call the (0, pi)-fragment. We then use a doubling construction to define a subtheory of KNOT, more specialised to standard encoding techniques in the defect braiding literature. Within this subtheory, we encompass standard braiding techniques by families of ribbon-like and tangle-like diagrams, each with semantics distinct from KNOT, in terms of the (0, pi)-fragment of ZX diagrams (again in the absence of byproducts). These subtheories may be used interoperably, and are each sound and complete for the (0, pi)-fragment of ZX diagrams. This provides a starting point to use the formal diagrammatics to analyse the operational effects of defect braiding procedures.

quant-ph↗
arXiv2025

Categories of sets with infinite addition

We consider sets with infinite addition, called $Σ$-monoids, and contribute to their literature in three ways. First, our definition subsumes those from previous works and allows us to relate them in terms of adjuctions between their categories. In particular, we discuss $Σ$-monoids with additive inverses. Second, we show that every Hausdorff commutative monoid is a $Σ$-monoid, and that there is a free Hausdorff commutative monoid for each $Σ$-monoid. Third, we prove that $Σ$-monoids have well-defined tensor products, unlike topological abelian groups.

math.CT↗
arXiv2024

Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime

Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated linearly by the type system, automatic uncomputation enables the programmer to treat it affinely to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz). Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.

cs.PL↗
arXiv2024

A Brief Review of Quantum Machine Learning for Financial Services

This review paper examines state-of-the-art algorithms and techniques in quantum machine learning with potential applications in finance. We discuss QML techniques in supervised learning tasks, such as Quantum Variational Classifiers, Quantum Kernel Estimation, and Quantum Neural Networks (QNNs), along with quantum generative AI techniques like Quantum Transformers and Quantum Graph Neural Networks (QGNNs). The financial applications considered include risk management, credit scoring, fraud detection, and stock price prediction. We also provide an overview of the challenges, potential, and limitations of QML, both in these specific areas and more broadly across the field. We hope that this can serve as a quick guide for data scientists, professionals in the financial sector, and enthusiasts in this area to understand why quantum computing and QML in particular could be interesting to explore in their field of expertise.

quant-ph↗
arXiv2024

Compositional Reversible Computation

Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing compositional reversible computation. We start from a historical perspective, by reviewing those approaches that developed reversible extensions of lambda-calculi, Turing machines, and communicating process calculi. These approaches share a common challenge: computations made reversible in this way do not naturally compose locally. We then turn our attention to computational models that eschew the detour via existing irreversible models. Building on an original analysis by Landauer, the insights of Bennett, Fredkin, and Toffoli introduced a fresh approach to reversible computing in which reversibility is elevated to the status of the main design principle. These initial models are expressed using low-level bit manipulations, however. Abstracting from the low-level of the Bennett-Fredkin-Toffoli models and pursuing more intrinsic, typed, and algebraic models, naturally leads to rig categories as the canonical model for compositional reversible programming. The categorical model reveals connections to type isomorphisms, symmetries, permutations, groups, and univalent universes. This, in turn, paves the way for extensions to reversible programming based on monads and arrows. These extensions are shown to recover conventional irreversible programming, a variety of reversible computational effects, and more interestingly both pure (measurement-free) and measurement-based quantum programming.

cs.LO↗
arXiv2023

Universal Properties of Partial Quantum Maps

We provide a universal construction of the category of finite-dimensional C*-algebras and completely positive trace-nonincreasing maps from the rig category of finite-dimensional Hilbert spaces and unitaries. This construction, which can be applied to any dagger rig category, is described in three steps, each associated with their own universal property, and draws on results from dilation theory in finite dimension. In this way, we explicitly construct the category that captures hybrid quantum/classical computation with possible nontermination from the category of its reversible foundations. We discuss how this construction can be used in the design and semantics of quantum programming languages.

quant-ph↗
arXiv2023

With a Few Square Roots, Quantum Computing is as Easy as Π

Rig groupoids provide a semantic model of \PiLang, a universal classical reversible programming language over finite types. We prove that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal and equationally sound and complete for a variety of gate sets. The first map corresponds to an $8^{\text{th}}$ root of the identity morphism on the unit $1$. The second map corresponds to a square root of the symmetry on $1+1$. As square roots are generally not unique and can sometimes even be trivial, the maps are constrained to satisfy a nondegeneracy axiom, which we relate to the Euler decomposition of the Hadamard gate. The semantic construction is turned into an extension of \PiLang, called \SPiLang, that is a computationally universal quantum programming language equipped with an equational theory that is sound and complete with respect to the Clifford gate set, the standard gate set of Clifford+T restricted to $\le 2$ qubits, and the computationally universal Gaussian Clifford+T gate set.

cs.PL↗