Introducing QWIRE, a quantum programming language based on linear type theory connected with intuitionistic type theory via the exponential modality:
Application to verified programming after implementation in Coq:
Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)
Robert Rand, Formally Verified Quantum Programming, UPenn (2018) [ediss:3175]
[p. iv:] “We argue that quantum programs demand machine-checkable proofs of correctness. We justify this on the basis of the complexity of programs manipulating quantum states, the expense of running quantum programs, and the inapplicability of traditional debugging techniques to programs whose states cannot be examined.”
[p. 3:] “Quantum programs are tremendously difficult to understand and implement, almost guaranteeing that they will have bugs. And traditional approaches to debugging will not help us: We cannot set breakpoints and look at our qubits without collapsing the quantum state. Even techniques like unit tests and random testing will be impossible to run on classical machines and too expensive to run on quantum computers – and failed tests are unlikely to be informative”
[p. 4:] “Thesis Statement: Quantum programming is not only amenable to formal verification: it demands it.”
“The overarching goal of this thesis is to write and verify quantum programs together. Towards that end, we introduce a quantum programming language called Qwire and embed it inside the Coq proof assistant. We give it a linear type system to ensure that it obeys the laws of quantum mechanics and a denotational semantics to prove that programs behave as desired.”
Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic, ReQWIRE: Reasoning about Reversible Quantum Circuits, EPTCS 287 (2019) 299-312 [arXiv:1901.10118, doi:10.4204/EPTCS.287.17]
Further on quantum circuit certification with the quantum programming language SQIR:
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks, A verified optimizer for Quantum circuits, Proceedings of the ACM on Programming Languages 5 Issue POPL 37 (2021) 1–29 [doi:10.1145/3434318]
Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks, Proving Quantum Programs Correct, in 12th International Conference on Interactive Theorem Proving (ITP 2021), Leibniz International Proceedings in Informatics (LIPIcs) 193 (2021) [arXiv:2010.01240]
On software verification for the ZX-calculus:
Adrian Lehmann, Ben Caldwell, Bhakti Shah, Robert Rand: VyZX: Formal Verification of a Graphical Quantum Language [arXiv:2311.11571]
Robert Rand: Verifying the ZX-calculus and its Friends, talk at Running HoTT 2024 [video:kt]
Last revised on July 14, 2024 at 13:04:47. See the history of this page for a list of all contributions to it.