constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
quantum algorithms:
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
QWIRE [Paykin, Rand & Zdancewic (2017)] is a quantum programming language for quantum circuit certification based on linear type theory combined with intuitionistic type theory via the exponential modality. More specifically, it is a domain specific programming language for quantum circuits meant to be embedded into an intuitionistic type theory. As such it is similar to Quipper.
The original article
Theoretical background:
Robert Rand, Formally Verified Quantum Programming, UPenn (2018) [ediss:3175]
emphasis on formal software verification:
[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.”
Jennifer Paykin, Linear/non-Linear Types For Embedded Domain-Specific Languages, 2018 (upenn:2752)
Application to verified programming after embedding into Coq:
Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266 (2018) 119-132 [arXiv:1803.00699]
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]
Using embedding into homotopy type theory:
For development EWIRE:
Fork development 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]
Kesha Hietala, A verified software toolchain for quantum programming (2022) [pdf, blog]
Last revised on February 23, 2023 at 16:02:03. See the history of this page for a list of all contributions to it.