Fri 17 Jun 2022 14:30 - 14:50 at Cockatoo - Special Effects Chair(s): Steven Holtzen

We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.

Fri 17 Jun

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:50
Special EffectsSIGPLAN Track at Cockatoo
Chair(s): Steven Holtzen Northeastern University
13:30
20m
Talk
(POPL 2022) Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
SIGPLAN Track
Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI Authorizer link Pre-print
13:50
20m
Talk
(ICFP 2020) Compiling effect handlers in capability-passing style
SIGPLAN Track
Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tuebingen
Link to publication DOI Authorizer link Pre-print
14:10
20m
Talk
(POPL 2021) Intensional Datatype Refinement
SIGPLAN Track
Eddie Jones University of Bristol, Steven Ramsay University of Bristol
14:30
20m
Talk
(POPL 2021) A Verified Optimizer for Quantum Circuits
SIGPLAN Track
Kesha Hietala University of Maryland, Robert Rand University of Chicago, Shih-Han Hung University of Maryland, USA, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD, Michael Hicks University of Maryland at College Park