QWIRE Practice: Formal Verification of Quantum Circuits in Coq. Rand, R., Paykin, J., & Zdancewic, S. In Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017), volume 266, pages 119–132, Waterloo, NSW, Australia, July, 2017. Open Publishing Association. ZSCC: NoCitationData[s1] arXiv: 1803.00699 Citation Key Alias: Rand2018a, rand2018
QWIRE Practice: Formal Verification of Quantum Circuits in Coq [link]Paper  doi  abstract   bibtex   
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.
@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}
}

Downloads: 0