Quantum references

TL;DR

This paper introduces a formal theory of quantum references that enables pointing to and manipulating parts of quantum systems, supporting formalization in theorem provers and applications in quantum programming.

Contribution

It develops a comprehensive framework for quantum references, including infinite-dimensional cases, and implements a quantum Hoare logic and teleportation analysis in Isabelle/HOL.

Findings

Framework for quantum references applicable to quantum variables and structures

Formalization of quantum references in theorem proving environments

Analysis of quantum teleportation using the developed theory

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.