September 21, 2023
Quantum computing is known to outperform classical computing on a certain set of tasks. That set, corresponding to the complexity class BQP, is still poorly understood by algorithms designers and theorists. One way to get a handle on quantum computing is to ask what we can program and what we can’t program. What kinds of quantum programs should a type system rule out? What kind of abstractions should a language provide? What should we aim to verify about a quantum program? Using the examples of the QUnity quantum-classical programming language and the VyZX verification tool, I’ll try to address some key challenges in understanding quantum computing and making it work in practice.
About Robert Rand
Robert Rand is an Assistant Professor of Computer Science at the University of Chicago. His research focuses on programming languages and verification for quantum computing and his main projects include the QWIRE quantum circuit language, the VOQC compiler for quantum circuits, and a stabilizer-based type system for quantum programs. He is currently developing tools for novel models of quantum computation, like the ZX-calculus and the one-way quantum computer. Robert developed and maintains the INQWIRE QuantumLib, an open-source library for verified quantum computing in the Coq proof assistant, which underlies many of his projects including his online textbook, Verified Quantum Computing.