A Coq-Based Infrastructure for Quantum Programming, Verification and Simulation

Quantum programming presents a significant departure from traditional programming due to its non-intuitive algorithm design and reliance on intricate linear algebraic derivations. Therefore, formal verification using theorem provers is essential and highly suitable for quantum programming. The mathematical foundation of quantum computing lies in matrix and vector computation. Hence, establishing a proper formal theory of matrices and vectors within theorem provers becomes of utmost significance. This paper expands and refines a Coq-based type system tailored for quantum computing, focusing specifically on powers-of-2 matrices and vectors. This enables precise descriptions of quantum states and operations while facilitating the formal verification of quantum programs. By utilizing this type system, we offer an environment for writing and verifying quantum programs. The verified programs can be extracted as equivalent OCaml files and executable simulators. Our work provides an effective infrastructure for quantum programming, verification and simulation, thereby laying a foundation for future developments.