QWIRE: A Core Language for Quantum Circuits
QWIRE: A Core Language for Quantum Circuits
Paykin, Rand, and Zdancewic introduce QWIRE, a typed circuit core with density-matrix semantics embedded in a classical host language.
Paper information (2017, POPL) — Jennifer Paykin, Robert Rand, and Steve Zdancewic. DOI; paper entry
Work
QWIRE is a core language for defining quantum circuits and embedding circuit manipulation in an arbitrary classical host language. It has only a few primitives, while the host language supplies modularity and expressiveness, reflecting the QRAM model in which a classical computer controls a quantum circuit. The paper gives a type system, operational semantics, and density-matrix denotational semantics, and studies safety and strong normalization when the host language has those properties.
Contributions
- A minimal circuit language embeddable in a classical host language.
- A type system and operational semantics with safety results.
- A density-matrix denotational semantics for circuits.
- Examples of host-language extensions for general circuit analysis and dependent types.
Limits
QWIRE's safety and strong-normalization results depend on assumptions about the host language; the core does not solve all hardware compilation, noise, resource-cost, or high-level algorithm-verification problems. Density-matrix semantics describes ideal circuit behavior and does not replace backend calibration or execution checks.
Connections
QWIRE combines Linear Type Systems with Quantum Circuits as an embeddable core and can be compared with the scalable circuit generation of Quipper. It continues the typed semantic direction of QPL and A Lambda Calculus for Quantum Computation with Classical Control, but centers circuit objects and the host-language interface.
Original paper
Jennifer Paykin, Robert Rand, and Steve Zdancewic, QWIRE: A Core Language for Quantum Circuits, in POPL 2017. DOI: 10.1145/3009837.3009894. Paper entry