Xiao-Ping Zhang, Department of Electrical, Computer & Biomedical Engineering
Matthew Amy, PhD candidate
David R. Cheriton School of Computer Science
The design and compilation of correct, efficient quantum circuits is integral to the future operation of quantum computers. This thesis makes contributions to the problems of optimizing and verifying quantum circuits, with an emphasis on the development of formal models for such purposes. We also present software implementations of these methods, which together form a full stack of tools for the design of optimized, formally verified quantum oracles.