Kesha HietalaRobert RandLiyi LiShih-Han HungXiaodi WuMichael Hicks2024-10-242024-10-242023-09-23https://scholars.lib.ntu.edu.tw/handle/123456789/722399<jats:p> We present <jats:sc>voqc</jats:sc> , the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called <jats:sc>sqir</jats:sc> , a small 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 <jats:sc>sqir</jats:sc> programs. <jats:sc>sqir</jats:sc> programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically to reason about programs that use an arbitrary number of quantum bits. <jats:sc>sqir</jats:sc> ’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in <jats:sc>voqc</jats:sc> , including full-circuit transformations from cutting-edge optimizers. </jats:p> <jats:p />journal article10.1145/3604630