
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Quantum Computing Algorithms and Architecture · Formal Methods in Verification
