Typed compositional quantum computation with lenses

TL;DR

The paper develops a compositional, type-theoretic framework for pure quantum circuits in Coq, leveraging lenses and focusing to separate circuit wiring from gate content and to curry states. Gates are modeled as natural transformations with uniform semantics, enabling generic, reuse-friendly proofs of circuit properties. The approach yields compositional correctness proofs for nontrivial circuits such as Shor's code and GHZ state preparation, without relying on explicit large Kronecker-product matrices. This yields scalable verification for quantum circuits and sets the stage for extensions to noisy channels, a formal theory of lenses, and deeper category-theoretic insights into focusing.

Abstract

We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows us to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally.

Figures (9)

• Figure 1: Shor's 9-qubit code
• Figure 2: Bit-flip code
• Figure 3: Sign-flip code
• Figure 4: Classical focusing
• Figure 5: Quantum focusing