This tutorial will introduce quantum computing to a programming languages audience through use of the Coq proof assistant. It will use the author’s recent Software Foundations-inspired textbook Verified Quantum Computing. Beyond introducing attendees to the basics of quantum computing, it will introduce a simple quantum programming language, called SQIR, and demonstrate how to verify the correctness of quantum programs.

By the end of the workshop, attendees will have a concrete understanding of core quantum computing concepts, including superposition, entanglement, and measurement, and be able to write and verify small quantum programs. (Basic familiarity with Coq or similar proof assistants will be assumed.)

More details and tutorial: materials: https://www.cs.umd.edu/~rrand/popl_2020/

I am a Basili postdoctoral fellow in Programming Languages at the University of Maryland and the Joint Center for Quantum Information and Computer Science. My main interest is in applying techniques from programming languages and formal verification to the domain of quantum computation. My PhD thesis revolved around QWIRE (“choir”), a quantum circuit language and verification tool that I developed jointly with Jennifer Paykin at the University of Pennsylvania. I’m working on Verified Quantum Computing, an introduction to quantum computing in the Coq proof assistant, and SQIRE, a verified intermediate representation for optimizing and compiling quantum programs.