@inproceedings{rand_qwire_2017,
	address = {Waterloo, NSW, Australia},
	title = {{QWIRE} {Practice}: {Formal} {Verification} of {Quantum} {Circuits} in {Coq}},
	volume = {266},
	shorttitle = {{QWIRE} {Practice}},
	url = {https://doi.org/10.4204/EPTCS.266.8},
	doi = {10/gf8skv},
	abstract = {We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs.},
	booktitle = {Proceedings 14th {International} {Conference} on {Quantum} {Physics} and {Logic} ({QPL} 2017)},
	publisher = {Open Publishing Association},
	author = {Rand, Robert and Paykin, Jennifer and Zdancewic, Steve},
	month = jul,
	year = {2017},
	note = {ZSCC: NoCitationData[s1] 
arXiv: 1803.00699
Citation Key Alias: Rand2018a, rand2018},
	keywords = {cs.ET, cs.LO, cs.PL},
	pages = {119--132}
}

{"_id":"K8zoTEcm2qnHy5f3w","bibbaseid":"rand-paykin-zdancewic-qwirepracticeformalverificationofquantumcircuitsincoq-2017","authorIDs":[],"author_short":["Rand, R.","Paykin, J.","Zdancewic, S."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Waterloo, NSW, Australia","title":"QWIRE Practice: Formal Verification of Quantum Circuits in Coq","volume":"266","shorttitle":"QWIRE Practice","url":"https://doi.org/10.4204/EPTCS.266.8","doi":"10/gf8skv","abstract":"We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs.","booktitle":"Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017)","publisher":"Open Publishing Association","author":[{"propositions":[],"lastnames":["Rand"],"firstnames":["Robert"],"suffixes":[]},{"propositions":[],"lastnames":["Paykin"],"firstnames":["Jennifer"],"suffixes":[]},{"propositions":[],"lastnames":["Zdancewic"],"firstnames":["Steve"],"suffixes":[]}],"month":"July","year":"2017","note":"ZSCC: NoCitationData[s1] arXiv: 1803.00699 Citation Key Alias: Rand2018a, rand2018","keywords":"cs.ET, cs.LO, cs.PL","pages":"119–132","bibtex":"@inproceedings{rand_qwire_2017,\n\taddress = {Waterloo, NSW, Australia},\n\ttitle = {{QWIRE} {Practice}: {Formal} {Verification} of {Quantum} {Circuits} in {Coq}},\n\tvolume = {266},\n\tshorttitle = {{QWIRE} {Practice}},\n\turl = {https://doi.org/10.4204/EPTCS.266.8},\n\tdoi = {10/gf8skv},\n\tabstract = {We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem proving features. The implementation uses higher-order abstract syntax to represent variable binding and provides a type-checking algorithm for linear wire types, ensuring that quantum circuits are well-formed. We formalize a denotational semantics that interprets QWIRE circuits as superoperators on density matrices, and prove the correctness of some simple quantum programs.},\n\tbooktitle = {Proceedings 14th {International} {Conference} on {Quantum} {Physics} and {Logic} ({QPL} 2017)},\n\tpublisher = {Open Publishing Association},\n\tauthor = {Rand, Robert and Paykin, Jennifer and Zdancewic, Steve},\n\tmonth = jul,\n\tyear = {2017},\n\tnote = {ZSCC: NoCitationData[s1] \narXiv: 1803.00699\nCitation Key Alias: Rand2018a, rand2018},\n\tkeywords = {cs.ET, cs.LO, cs.PL},\n\tpages = {119--132}\n}\n\n","author_short":["Rand, R.","Paykin, J.","Zdancewic, S."],"key":"rand_qwire_2017","id":"rand_qwire_2017","bibbaseid":"rand-paykin-zdancewic-qwirepracticeformalverificationofquantumcircuitsincoq-2017","role":"author","urls":{"Paper":"https://doi.org/10.4204/EPTCS.266.8"},"keyword":["cs.ET","cs.LO","cs.PL"],"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.524Z","downloads":0,"keywords":["cs.et","cs.lo","cs.pl"],"search_terms":["qwire","practice","formal","verification","quantum","circuits","coq","rand","paykin","zdancewic"],"title":"QWIRE Practice: Formal Verification of Quantum Circuits in Coq","year":2017,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}