Title: Applications of Hoare Logic for Quantum Compiler Optimizations

Abstract: To keep noise to a minimum on NISQ-era hardware, it is crucial to reduce the circuit size of quantum programs as much as possible. As hand-optimized circuits become increasingly infeasible with rising complexity, we turn to compilers to perform these optimizations for us. In this novel approach to automated circuit optimizations, we use Hoare Logic (traditionally used to show program correctness) to identify advanced optimization opportunities. By tracking guarantees on the state of qubits after each operation, the compiler obtains valuable information that is used to eliminate superfluous operations. One advantage of this approach is its applicability to various levels of abstraction from very low-level gates to high-level subroutines. In addition to providing an implementation in the open-source compilation systems ProjectQ & Qiskit, the framework was extended with an optimization technique able to drastically reduce the T-count of Toffoli gates, which becomes relevant in surface code settings.