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.

翻译：我们提出了一种"量子引用"理论，类似于经典函数式编程中的透镜，允许指向较大量子系统的子系统，并对该部分进行突变/测量。可变的经典变量、量子寄存器以及量子电路中的导线都是其示例，同时也包括对较大量子数据结构中部分的引用。在我们的设定中，量子引用还可以指向其他引用的子部分、不同引用中部分的组合，或以不同基表示的量子引用等。我们的建模旨在很好地适用于定理证明器中的形式化，并作为量子程序中变量建模的基础。我们更详细地研究了量子引用，并涵盖了无限维情况，同时也提供了不特定于量子情况的更一般性处理。我们在Isabelle/HOL定理证明器中实现了我们结果的大部分内容（包括一个小的量子霍尔逻辑和量子隐形传态分析）。