Back to Search
Start Over
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- Source :
- Electronic Proceedings in Theoretical Computer Science, Vol 266, Iss Proc. QPL 2017, Pp 119-132 (2018)
- Publication Year :
- 2018
- Publisher :
- Open Publishing Association, 2018.
-
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.
- Subjects :
- Mathematics
QA1-939
Electronic computers. Computer science
QA75.5-76.95
Subjects
Details
- Language :
- English
- ISSN :
- 20752180
- Volume :
- 266
- Issue :
- Proc. QPL 2017
- Database :
- Directory of Open Access Journals
- Journal :
- Electronic Proceedings in Theoretical Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- edsdoj.f407acf1db94a06a933dd8398b41c9e
- Document Type :
- article
- Full Text :
- https://doi.org/10.4204/EPTCS.266.8