Dependent Type Theory for Verified Quantum Software

Interactive theorem proving has emerged as a potent technology for formalized mathematics in general, and formal program verification in particular. It produces machine-checkable proofs that offer a very high degree of confidence in the correctness of the proved results. Among the various approaches to interactive theorem proving, dependent type theory is particularly suitable for software analysis. We will develop dependent type theories for reasoning about quantum software. In the context of quantum computing, formal verification takes on added importance, because other techniques for ensuring the correctness of software, such as debugging by setting break points and inspecting the program state, are not in general applicable in a quantum setting. Since machine-checkable proofs are more reliable and more re-usable than proofs done by hand, the hope is that they may eventually be employed in the verification of security properties of distributed quantum programs. Our investigation will focus on four main areas: specification of quantum software, quantum circuit programming with enhanced circuit operations, the semantics of quantum programming languages, and proof assistant support for syntax with binders. We will build upon dependently typed Proto-Quipper, a prototype quantum programming language based on linear logic and dependent type theory. Proto-Quipper has a strong type system, which makes programs safer, easier to analyze, and less costly to debug. We will extend the Proto-Quipper type system to allow properties of quantum programs to be directly expressed as types in the programming language. We also plan to a novel proof assistant based on a com bination of dependent types and the theory of nominal sets, and to use it to formalize some of the metatheory of programming languages and to prove program correctness properties.