Quantum computing is a challenging domain, both conceptually and for writing correct programs, and a prime target for formal verification. This tutorial will serve as a basic introduction towards using the Coq proof assistant to learn quantum computing and prove the correctness of quantum programs. We will use the online, interactive textbook VQC for a two-part tutorial. The first session will cover the foundations of quantum computing, with a focus on complex numbers, linear algebra, and qubit entanglement. The second session will verifying quantum programs written in a small imperative quantum language. By the end of the tutorial attendees will have a beginner’s understanding of quantum computing and how to verify quantum programs. The textbook itself will be available publicly and can serve as a simple 1-2 week course, either by itself or as part of a course in formal verification. A basic understanding of the Coq proof assistant will be assumed.
