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...

Full description

Bibliographic Details
Main Authors: Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic
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
id doaj-458893be75f44370a4675a0bc3b8d22e
record_format Article
spelling doaj-458893be75f44370a4675a0bc3b8d22e2020-11-25T02:43:14ZengOpen 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
collection DOAJ
language English
format Article
sources DOAJ
author Robert Rand
Jennifer Paykin
Dong-Ho Lee
Steve Zdancewic
spellingShingle Robert Rand
Jennifer Paykin
Dong-Ho Lee
Steve Zdancewic
ReQWIRE: Reasoning about Reversible Quantum Circuits
Electronic Proceedings in Theoretical Computer Science
author_facet Robert Rand
Jennifer Paykin
Dong-Ho Lee
Steve Zdancewic
author_sort Robert Rand
title ReQWIRE: Reasoning about Reversible Quantum Circuits
title_short 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_sort reqwire: reasoning about reversible quantum circuits
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2019-01-01
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.
url http://arxiv.org/pdf/1901.10118v1
work_keys_str_mv AT robertrand reqwirereasoningaboutreversiblequantumcircuits
AT jenniferpaykin reqwirereasoningaboutreversiblequantumcircuits
AT dongholee reqwirereasoningaboutreversiblequantumcircuits
AT stevezdancewic reqwirereasoningaboutreversiblequantumcircuits
_version_ 1724770609544560640