Quantum algorithms can solve some problems exponentially faster than classical algorithms and the quantum computers that can run them are rapidly getting better. However, implementing a quantum algorithm on a quantum computer is a difficult task that could use some tool support. Such tools are emerging and more are needed, particularly for optimization and verification of quantum programs. The challenge is to design tools that run in polynomial time, which is in contrast to simulation which takes exponential time, in general. I will present approaches to the optimization and verification of quantum programs that scale to large programs. Our optimizer uses an automatically generated set of local rules and is competitive with the state of the art. Our verifier uses abstract interpretation with an abstract domain of polynomial size and is the first that can verify certain assertions automatically. My presentation is based on papers in PLDI 2021 and PLDI 2022.

Jens Palsberg is a Professor and former Department Chair of Computer Science at the University of California, Los Angeles (UCLA). His research interests span the areas of programming languages, software engineering, and quantum computing. He is the director of the UCLA-Amazon Science Hub for Humanity and Artificial Intelligence, an associate editor of ACM Transactions on Quantum Computing, and a member of the ACM Executive Committee. In 2012 he received the ACM SIGPLAN Distinguished Service Award, and in 2023 he received the Eon Instrumentation Excellence in Teaching Award at UCLA for his courses on quantum computing.