@article{Hietala2021,
  title         = {A Verified Optimizer for {{Quantum}} Circuits},
  author        = {Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Wu, Xiaodi and Hicks, Michael},
  year          = {2021},
  month         = jan,
  journal       = pacmpl,
  volume        = {5},
  number        = {POPL},
  eid           = {37},
  pages         = {37},
  doi           = {10.1145/3434318},
  archiveprefix = {arXiv},
  eprint        = {1912.02250},
  url           = {https://github.com/inQWIRE/SQIR},
  abstract      = {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.},
  keywords      = {programming languages, formal verification, certified compilation, quantum computing, circuit optimization},
  webnote       = {POPL '21. See arXiv version for full paper with appendix.},
  bibsource     = qplbib
}

{"_id":"eLbNDSYiHcLAMSwcu","bibbaseid":"hietala-rand-hung-wu-hicks-averifiedoptimizerforquantumcircuits-2021","author_short":["Hietala, K.","Rand, R.","Hung, S.","Wu, X.","Hicks, M."],"bibdata":{"bibtype":"article","type":"article","title":"A Verified Optimizer for Quantum Circuits","author":[{"propositions":[],"lastnames":["Hietala"],"firstnames":["Kesha"],"suffixes":[]},{"propositions":[],"lastnames":["Rand"],"firstnames":["Robert"],"suffixes":[]},{"propositions":[],"lastnames":["Hung"],"firstnames":["Shih-Han"],"suffixes":[]},{"propositions":[],"lastnames":["Wu"],"firstnames":["Xiaodi"],"suffixes":[]},{"propositions":[],"lastnames":["Hicks"],"firstnames":["Michael"],"suffixes":[]}],"year":"2021","month":"January","journal":"Proceedings of the ACM on Programming Languages","volume":"5","number":"POPL","eid":"37","pages":"37","doi":"10.1145/3434318","archiveprefix":"arXiv","eprint":"1912.02250","url":"https://github.com/inQWIRE/SQIR","abstract":"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.","keywords":"programming languages, formal verification, certified compilation, quantum computing, circuit optimization","webnote":"POPL '21. See arXiv version for full paper with appendix.","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@article{Hietala2021,\n title = {A Verified Optimizer for {{Quantum}} Circuits},\n author = {Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Wu, Xiaodi and Hicks, Michael},\n year = {2021},\n month = jan,\n journal = pacmpl,\n volume = {5},\n number = {POPL},\n eid = {37},\n pages = {37},\n doi = {10.1145/3434318},\n archiveprefix = {arXiv},\n eprint = {1912.02250},\n url = {https://github.com/inQWIRE/SQIR},\n abstract = {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.},\n keywords = {programming languages, formal verification, certified compilation, quantum computing, circuit optimization},\n webnote = {POPL '21. See arXiv version for full paper with appendix.},\n bibsource = qplbib\n}\n\n","author_short":["Hietala, K.","Rand, R.","Hung, S.","Wu, X.","Hicks, M."],"key":"Hietala2021","id":"Hietala2021","bibbaseid":"hietala-rand-hung-wu-hicks-averifiedoptimizerforquantumcircuits-2021","role":"author","urls":{"Paper":"https://github.com/inQWIRE/SQIR"},"keyword":["programming languages","formal verification","certified compilation","quantum computing","circuit optimization"],"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","dataSources":["MbqeeC74KZhwBpe8j","JG9W34HAXfSxsC6ML"],"keywords":["programming languages","formal verification","certified compilation","quantum computing","circuit optimization"],"search_terms":["verified","optimizer","quantum","circuits","hietala","rand","hung","wu","hicks"],"title":"A Verified Optimizer for Quantum Circuits","year":2021}