ReQWIRE: Reasoning about Reversible Quantum Circuits
Common quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit languages let programmers assert that a qubit has been returned to the |0> state before it is discarded, allowing for a...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1901.10118v1 |
| _version_ | 1818596810157981696 |
|---|---|
| author | Robert Rand Jennifer Paykin Dong-Ho Lee Steve Zdancewic |
| author_facet | Robert Rand Jennifer Paykin Dong-Ho Lee Steve Zdancewic |
| author_sort | Robert Rand |
| collection | DOAJ |
| description | Common quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit languages let programmers assert that a qubit has been returned to the |0> state before it is discarded, allowing for a range of optimizations. However, existing languages do not provide the tools to verify these assertions, introducing a potential source of errors. In this paper we present methods for verifying that ancillae are discarded in the desired state, and use these methods to implement a verified compiler from classical functions to quantum oracles. |
| first_indexed | 2024-12-16T11:37:49Z |
| format | Article |
| id | doaj.art-458893be75f44370a4675a0bc3b8d22e |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-16T11:37:49Z |
| publishDate | 2019-01-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-458893be75f44370a4675a0bc3b8d22e2022-12-21T22:33:01ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-01-01287Proc. QPL 201829931210.4204/EPTCS.287.17:26ReQWIRE: Reasoning about Reversible Quantum CircuitsRobert RandJennifer PaykinDong-Ho LeeSteve ZdancewicCommon quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that state and discarded. Existing quantum circuit languages let programmers assert that a qubit has been returned to the |0> state before it is discarded, allowing for a range of optimizations. However, existing languages do not provide the tools to verify these assertions, introducing a potential source of errors. In this paper we present methods for verifying that ancillae are discarded in the desired state, and use these methods to implement a verified compiler from classical functions to quantum oracles.http://arxiv.org/pdf/1901.10118v1 |
| spellingShingle | Robert Rand Jennifer Paykin Dong-Ho Lee Steve Zdancewic ReQWIRE: Reasoning about Reversible Quantum Circuits Electronic Proceedings in Theoretical Computer Science |
| title | ReQWIRE: Reasoning about Reversible Quantum Circuits |
| title_full | ReQWIRE: Reasoning about Reversible Quantum Circuits |
| title_fullStr | ReQWIRE: Reasoning about Reversible Quantum Circuits |
| title_full_unstemmed | ReQWIRE: Reasoning about Reversible Quantum Circuits |
| title_short | ReQWIRE: Reasoning about Reversible Quantum Circuits |
| title_sort | reqwire reasoning about reversible quantum circuits |
| url | http://arxiv.org/pdf/1901.10118v1 |
| work_keys_str_mv | AT robertrand reqwirereasoningaboutreversiblequantumcircuits AT jenniferpaykin reqwirereasoningaboutreversiblequantumcircuits AT dongholee reqwirereasoningaboutreversiblequantumcircuits AT stevezdancewic reqwirereasoningaboutreversiblequantumcircuits |