QWIRE Practice: Formal Verification of Quantum Circuits in Coq

Paykin, Jennifer ; Rand, Robert ; et al.

In: Electronic Proceedings in Theoretical Computer Science, Jg. 266 (2018), Heft Proc. QPL 2017, S. 119-132

Online unknown

Zugriff:

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.

Comment: In Proceedings QPL 2017, arXiv:1802.09737

Titel:	QWIRE Practice: Formal Verification of Quantum Circuits in Coq
Autor/in / Beteiligte Person:	Paykin, Jennifer ; Rand, Robert ; Zdancewic, Steve
Link:	View record in OpenAIRE (Volltext)
Zeitschrift:	Electronic Proceedings in Theoretical Computer Science, Jg. 266 (2018), Heft Proc. QPL 2017, S. 119-132
Veröffentlichung:	arXiv, 2018
Medientyp:	unknown
DOI:	10.48550/arxiv.1803.00699
Schlagwort:	FOS: Computer and information sciences Computer Science - Logic in Computer Science Correctness Computer science Computer Science - Emerging Technologies 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences lcsh:QA75.5-76.95 Quantum circuit Computer Science::Hardware Architecture Denotational semantics Computer Science::Emerging Technologies Abstract syntax 0202 electrical engineering, electronic engineering, information engineering Quantum Formal verification Computer Science - Programming Languages Programming language lcsh:Mathematics Proof assistant D.2.4 020207 software engineering lcsh:QA1-939 Logic in Computer Science (cs.LO) Automated theorem proving Emerging Technologies (cs.ET) F.3.1 010201 computation theory & mathematics Computer Science::Programming Languages lcsh:Electronic computers. Computer science computer Programming Languages (cs.PL)
Sonstiges:	Nachgewiesen in: OpenAIRE Rights: OPEN

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.