QWIRE Practice: Formal Verification of Quantum Circuits in Coq

QWIRE Practice: Formal Verification of Quantum Circuits in Coq

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 abstrac...

Full description

Bibliographic Details
Main Authors: Robert Rand, Jennifer Paykin, Steve Zdancewic
Format: Article
Language:English
Published: Open Publishing Association 2018-02-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1803.00699v1
id doaj-af407acf1db94a06a933dd8398b41c9e
record_format Article
spelling doaj-af407acf1db94a06a933dd8398b41c9e2020-11-25T02:11:02ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-02-01266Proc. QPL 201711913210.4204/EPTCS.266.8:45QWIRE Practice: Formal Verification of Quantum Circuits in CoqRobert Rand0Jennifer Paykin1Steve Zdancewic2 University of Pennsylvania University of Pennsylvania University of Pennsylvania 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.http://arxiv.org/pdf/1803.00699v1
collection DOAJ
language English
format Article
sources DOAJ
author Robert Rand
Jennifer Paykin
Steve Zdancewic
spellingShingle Robert Rand
Jennifer Paykin
Steve Zdancewic
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
Electronic Proceedings in Theoretical Computer Science
author_facet Robert Rand
Jennifer Paykin
Steve Zdancewic
author_sort Robert Rand
title QWIRE Practice: Formal Verification of Quantum Circuits in Coq
title_short QWIRE Practice: Formal Verification of Quantum Circuits in Coq
title_full QWIRE Practice: Formal Verification of Quantum Circuits in Coq
title_fullStr QWIRE Practice: Formal Verification of Quantum Circuits in Coq
title_full_unstemmed QWIRE Practice: Formal Verification of Quantum Circuits in Coq
title_sort qwire practice: formal verification of quantum circuits in coq
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2018-02-01
description 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.
url http://arxiv.org/pdf/1803.00699v1
work_keys_str_mv AT robertrand qwirepracticeformalverificationofquantumcircuitsincoq
AT jenniferpaykin qwirepracticeformalverificationofquantumcircuitsincoq
AT stevezdancewic qwirepracticeformalverificationofquantumcircuitsincoq
_version_ 1724916782216511488

Similar Items