ReQWIRE: Reasoning about Reversible Quantum Circuits. Rand, R., Paykin, J., Lee, D., & Zdancewic, S. Electronic Proceedings in Theoretical Computer Science, 287:299–312, January, 2019. ZSCC: 0000005 arXiv: 1901.10118
ReQWIRE: Reasoning about Reversible Quantum Circuits [link]Paper  doi  abstract   bibtex   
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 \textbar0\textgreater 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.
@article{rand_reqwire:_2019,
	title = {{ReQWIRE}: {Reasoning} about {Reversible} {Quantum} {Circuits}},
	volume = {287},
	issn = {2075-2180},
	shorttitle = {{ReQWIRE}},
	url = {http://arxiv.org/abs/1901.10118},
	doi = {10/ggb9c2},
	abstract = {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 {\textbar}0{\textgreater} 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.},
	urldate = {2019-11-01},
	journal = {Electronic Proceedings in Theoretical Computer Science},
	author = {Rand, Robert and Paykin, Jennifer and Lee, Dong-Ho and Zdancewic, Steve},
	month = jan,
	year = {2019},
	note = {ZSCC: 0000005 
arXiv: 1901.10118},
	keywords = {Computer Science - Emerging Technologies, Computer Science - Logic in Computer Science, Computer Science - Programming Languages},
	pages = {299--312}
}

Downloads: 0