  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.
