@inproceedings{Rand2019,
  title      = {{{ReQWIRE}}: {{Reasoning}} about {{Reversible Quantum Circuits}}},
  shorttitle = {{{ReQWIRE}}},
  author     = {Rand, Robert and Paykin, Jennifer and Lee, Dongho and Zdancewic, Steve},
  year       = {2019},
  month      = jan,
  booktitle  = {Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL), Halifax, Canada, June 3--7, 2018},
  editor     = {Selinger, Peter and Chiribella, Giulio},
  publisher  = opa,
  address    = {Waterloo, NSW, Australia},
  series     = eptcs,
  volume     = {287},
  pages      = {299--312},
  doi        = {10.4204/EPTCS.287.17},
  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 |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.},
  bibsource  = qplbib
}

{"_id":"3GMDD73b2GD53pSDm","bibbaseid":"rand-paykin-lee-zdancewic-reqwirereasoningaboutreversiblequantumcircuits-2019","authorIDs":[],"author_short":["Rand, R.","Paykin, J.","Lee, D.","Zdancewic, S."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"ReQWIRE: Reasoning about Reversible Quantum Circuits","shorttitle":"ReQWIRE","author":[{"propositions":[],"lastnames":["Rand"],"firstnames":["Robert"],"suffixes":[]},{"propositions":[],"lastnames":["Paykin"],"firstnames":["Jennifer"],"suffixes":[]},{"propositions":[],"lastnames":["Lee"],"firstnames":["Dongho"],"suffixes":[]},{"propositions":[],"lastnames":["Zdancewic"],"firstnames":["Steve"],"suffixes":[]}],"year":"2019","month":"January","booktitle":"Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL), Halifax, Canada, June 3–7, 2018","editor":[{"propositions":[],"lastnames":["Selinger"],"firstnames":["Peter"],"suffixes":[]},{"propositions":[],"lastnames":["Chiribella"],"firstnames":["Giulio"],"suffixes":[]}],"publisher":"Open Publishing Association","address":"Waterloo, NSW, Australia","series":"Electronic Proceedings in Theoretical Computer Science","volume":"287","pages":"299–312","doi":"10.4204/EPTCS.287.17","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 |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.","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@inproceedings{Rand2019,\n title = {{{ReQWIRE}}: {{Reasoning}} about {{Reversible Quantum Circuits}}},\n shorttitle = {{{ReQWIRE}}},\n author = {Rand, Robert and Paykin, Jennifer and Lee, Dongho and Zdancewic, Steve},\n year = {2019},\n month = jan,\n booktitle = {Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL), Halifax, Canada, June 3--7, 2018},\n editor = {Selinger, Peter and Chiribella, Giulio},\n publisher = opa,\n address = {Waterloo, NSW, Australia},\n series = eptcs,\n volume = {287},\n pages = {299--312},\n doi = {10.4204/EPTCS.287.17},\n 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 |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.},\n bibsource = qplbib\n}\n\n","author_short":["Rand, R.","Paykin, J.","Lee, D.","Zdancewic, S."],"editor_short":["Selinger, P.","Chiribella, G."],"key":"Rand2019","id":"Rand2019","bibbaseid":"rand-paykin-lee-zdancewic-reqwirereasoningaboutreversiblequantumcircuits-2019","role":"author","urls":{},"metadata":{"authorlinks":{}},"downloads":0},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","creationDate":"2020-05-31T17:07:22.666Z","downloads":0,"keywords":[],"search_terms":["reqwire","reasoning","reversible","quantum","circuits","rand","paykin","lee","zdancewic"],"title":"ReQWIRE: Reasoning about Reversible Quantum Circuits","year":2019,"dataSources":["Z5Dp3qAJiMzxtvKMq","JG9W34HAXfSxsC6ML"]}