Current browse context:
cs.PL
Change to browse by:
References & Citations
Computer Science > Programming Languages
Title: A Verified Optimizer for Quantum Circuits
(Submitted on 4 Dec 2019 (this version), latest version 13 Nov 2020 (v3))
Abstract: We present VOQC, the first fully verified compiler for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. We evaluate VOQC's verified optimizations on a series of benchmarks, and it performs comparably to industrial-strength compilers. VOQC's optimizations reduce total gate counts on average by 17.7% on a benchmark of 29 circuit programs compared to a 10.7% reduction when using IBM's Qiskit compiler.
Submission history
From: Kesha Hietala [view email][v1] Wed, 4 Dec 2019 21:07:00 GMT (558kb,D)
[v2] Sat, 25 Apr 2020 16:54:52 GMT (3563kb,D)
[v3] Fri, 13 Nov 2020 02:45:31 GMT (1806kb,D)
Link back to: arXiv, form interface, contact.