Quantum references

TL;DR

The paper introduces quantum references, a semantic foundation that points to and modifies subsystems within a larger quantum state, analogous to lenses in classical programming. It develops a generic, axiomatic theory of references and then instantiates it to finite- and infinite-dimensional quantum systems as well as classical systems, enabling modular programming language semantics and formal verification. A key contribution is the formal Isabelle/HOL development, including a small quantum Hoare logic and the teleportation protocol, plus a comprehensive lifting framework that relates quantum objects (unitaries, channels, measurements, subspaces) to their memory-wide counterparts. The work bridges programming language semantics with quantum theory, offering tools for reasoning about variables, memory, and subsystems in quantum programs, and it lays groundwork for future mixed classical/quantum references and optics-related connections. Overall, it provides a rigorous semantic foundation for first-class quantum references and demonstrates practical applicability through formalization and verified results.

Abstract

We present a theory of "quantum references", similar to lenses in classical functional programming, that allow to point to a subsystem of a larger quantum system, and to mutate/measure that part. Mutable classical variables, quantum registers, and wires in quantum circuits are examples of this, but also references to parts of larger quantum datastructures. Quantum references in our setting can also refer to subparts of other references, or combinations of parts from different references, or quantum references seen in a different basis, etc. Our modeling is intended to be well suited for formalization in theorem provers and as a foundation for modeling variables in quantum programs. We study quantum references in greater detail and cover the infinite-dimensional case as well, but also provide a more general treatment not specific to the quantum case. We implemented a large part of our results (including a small quantum Hoare logic and an analysis of quantum teleportation) in the Isabelle/HOL theorem prover.

Figures (5)

• Figure 1: Axioms for a reference category $\calR$
• Figure 2: Generic (derived) laws for references. All laws have the implicit assumption that the domains/codomains of the references match. (E.g., if $\chain FG$ occurs in a law, then the domain of $F$ is assumed to match the codomain of $G$.) The proofs of these laws (as a consequence of the axioms in \ref{['fig:axioms']}) are given in \ref{['sec:proofs:laws']}.
• Figure 3: Teleportation circuit and program. $\symbolindexmarkhighlightGRAYBOX\hada$ is the Hadamard matrix, $\symbolindexmarkhighlightGRAYBOX\pauliX$ is the Pauli-$X$ matrix, and $\symbolindexmarkhighlightGRAYBOX\pauliZ$ is the Pauli-$Z$ matrix.
• Figure 4: Additional laws in a reference category with complements. All laws have the implicit assumption that the types of the references match.
• Figure 5: Isabelle/HOL theories References-AFP. Lines of code are without blanks or comments.

Theorems & Definitions (91)

• Definition 1
• Definition 2: Chaining
• Definition 3: Compatibility / pairs
• Lemma 1
• Theorem 1
• Lemma 2
• proof
• Lemma 3
• Lemma 4
• Lemma 5