{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:16Z","timestamp":1775790796723,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,9,23]],"date-time":"2023-09-23T00:00:00Z","timestamp":1695427200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, Quantum Testbed Pathfinder Program","award":["DE-SC0019040"],"award-info":[{"award-number":["DE-SC0019040"]}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA95502110051"],"award-info":[{"award-number":["FA95502110051"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2023,9,30]]},"abstract":"<jats:p>\n            We present\n            <jats:sc>voqc<\/jats:sc>\n            , 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\n            <jats:sc>sqir<\/jats:sc>\n            , 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\n            <jats:sc>sqir<\/jats:sc>\n            programs.\n            <jats:sc>sqir<\/jats:sc>\n            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.\n            <jats:sc>sqir<\/jats:sc>\n            \u2019s careful design and our provided automation make it possible to write and verify a broad range of optimizations in\n            <jats:sc>voqc<\/jats:sc>\n            , including full-circuit transformations from cutting-edge optimizers.\n          <\/jats:p>\n          <jats:p\/>","DOI":"10.1145\/3604630","type":"journal-article","created":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T12:28:02Z","timestamp":1689164882000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["A Verified Optimizer for Quantum Circuits"],"prefix":"10.1145","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2724-0974","authenticated-orcid":false,"given":"Kesha","family":"Hietala","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6842-5505","authenticated-orcid":false,"given":"Robert","family":"Rand","sequence":"additional","affiliation":[{"name":"University of Chicago, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-0244","authenticated-orcid":false,"given":"Liyi","family":"Li","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3410-7466","authenticated-orcid":false,"given":"Shih-Han","family":"Hung","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8877-9802","authenticated-orcid":false,"given":"Xiaodi","family":"Wu","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2759-9223","authenticated-orcid":false,"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,9,23]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"Matthew Amy. 2018. Towards Large-Scale Functional Verification of Universal Quantum Circuits. arXiv:1805.06908 (2018)."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab9359"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2341953"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_1"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/QCE49297.2020.00051"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"e_1_3_3_9_2","unstructured":"Cambridge Quantum Computing Ltd. 2019. pytket. Retrieved July 17 2023 from https:\/\/cqcl.github.io\/tket\/pytket\/api\/index.html"},{"key":"e_1_3_3_10_2","unstructured":"Chair for Design Automation at the Technical University of Munich. 2022. MQT QMAP\u2014A Tool for Quantum Circuit Mapping Written in C++. Retrieved July 17 2023 from https:\/\/github.com\/cda-tum\/qmap"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TQC.2019.3"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3476303"},{"key":"e_1_3_3_13_2","unstructured":"Andrew W. Cross Lev S. Bishop John A. Smolin and Jay M. Gambetta. 2017. Open quantum assembly language. arXiv:1707.03429 (2017). https:\/\/github.com\/Qiskit\/openqasm\/tree\/OpenQASM2.x"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4586899"},{"key":"e_1_3_3_15_2","unstructured":"David Eberly. 1999. Euler Angle Formulas. Retrieved July 17 2023 from https:\/\/www.geometrictools.com\/Documentation\/EulerAngles.pdf"},{"key":"e_1_3_3_16_2","volume-title":"Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL\u201918)","author":"Fagan Andrew","year":"2018","unstructured":"Andrew Fagan and Ross Duncan. 2018. Optimising Clifford circuits with quantomatic. In Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL\u201918)."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0849-4_10"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aad604"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.21"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_3_3_22_2","unstructured":"IBM. 2022. IBM Quantum Processor Types. Retrieved July 17 2023 from https:\/\/quantum-computing.ibm.com\/lab\/docs\/iql\/manage\/systems\/processors"},{"key":"e_1_3_3_23_2","article-title":"Interfacing C with OCaml","year":"2021","unstructured":"INRIA. 2021. Interfacing C with OCaml. Retrieved April 9, 2021 from https:\/\/ocaml.org\/manual\/intfc.html","journal-title":"https:\/\/ocaml.org\/manual\/intfc.html"},{"key":"e_1_3_3_24_2","unstructured":"INRIA. 2022. Library Coq.Reals.Reals. Retrieved March 23 2022 from https:\/\/coq.inria.fr\/library\/Coq.Reals.Reals.html"},{"key":"e_1_3_3_25_2","article-title":"Program Extraction","author":"Letouzey Jean-Christophe Filliatre and Pierre","year":"2021","unstructured":"Jean-Christophe Filliatre and Pierre Letouzey. 2021. Program Extraction. Retrieved September 24, 2021 from https:\/\/coq.inria.fr\/refman\/addendum\/extraction.html","journal-title":"R"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3491247"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_3_3_28_2","volume-title":"Proceedings of the 16th International Conference on Quantum Physics and Logic (QPL\u201919)","author":"Kissinger Aleks","year":"2019","unstructured":"Aleks Kissinger and John van de Wetering. 2019. PyZX: Large scale automated diagrammatic reasoning. In Proceedings of the 16th International Conference on Quantum Physics and Logic (QPL\u201919)."},{"key":"e_1_3_3_29_2","unstructured":"Aleks Kissinger and John van de Wetering. 2019. Reducing T-count with the ZX-calculus. arXiv e-prints arXiv:1903.10477 [quant-ph] (2019)."},{"key":"e_1_3_3_30_2"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304023"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507715"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563309"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2006.35"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41534-018-0072-4"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.2218775120"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_3_3_38_2","article-title":"ctypes\u2014A Foreign Function Library for Python","author":"Foundation Python Software","year":"2021","unstructured":"Python Software Foundation. 2021. ctypes\u2014A Foreign Function Library for Python. Retrieved April 9, 2021 from https:\/\/docs.python.org\/3\/library\/ctypes.html","journal-title":"https:\/\/docs.python.org\/3\/library\/ctypes.html"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2562110"},{"key":"e_1_3_3_40_2","article-title":"Transpiler Passes (qiskit.transpiler.passes)","author":"Team Qiskit Development","year":"2021","unstructured":"Qiskit Development Team. 2021. Transpiler Passes (qiskit.transpiler.passes). Retrieved April 5, 2021 from https:\/\/qiskit.org\/documentation\/apidoc\/transpiler_passes.html","journal-title":"R"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.8"},{"key":"e_1_3_3_42_2","unstructured":"Rigetti Computing. 2019. Welcome to the Docs for pyQuil! Retrieved July 17 2023 fromhttp:\/\/pyquil.readthedocs.io\/en\/latest\/"},{"key":"e_1_3_3_43_2","unstructured":"Rigetti Computing. 2019. The @rigetti Optimizing Quil Compiler. Retrieved July 17 2023 from https:\/\/github.com\/rigetti\/quilc"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11128-010-0201-2"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab8e92"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322262"},{"key":"e_1_3_3_47_2","unstructured":"Robert S. Smith Michael J. Curtis and William J. Zeng. 2016. A practical quantum instruction set architecture. arXiv:1608.03355 (2016)."},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-01-31-49"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304007"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_3_51_2","volume-title":"INQWIRE QuantumLib","author":"Developers The INQWIRE","year":"2022","unstructured":"The INQWIRE Developers. 2022. INQWIRE QuantumLib. Retrieved July 17, 2023 from https:\/\/github.com\/inQWIRE\/QuantumLib"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.69.032315"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3316781.3317859"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2008.43"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_3_3_56_2","doi-asserted-by":"crossref","unstructured":"Alwin Zulehner Alexandru Paler and Robert Wille. 2017. An efficient methodology for mapping quantum circuits to the IBM QX architectures. arXiv e-prints arXiv:1712.04722 [quant-ph] (2017).","DOI":"10.23919\/DATE.2018.8342181"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3604630","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3604630","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:04Z","timestamp":1750178764000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3604630"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,23]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9,30]]}},"alternative-id":["10.1145\/3604630"],"URL":"https:\/\/doi.org\/10.1145\/3604630","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,23]]},"assertion":[{"value":"2022-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-05-10","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}