{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T01:05:22Z","timestamp":1783991122390,"version":"3.55.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0019040"],"award-info":[{"award-number":["DE-SC0019040"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA95502110051 and FA95502110209"],"award-info":[{"award-number":["FA95502110051 and FA95502110209"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum program. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits between two different bases via the quantum Fourier transform, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM\u2019s design enabled us to prove correct VQO\u2019s compilers\u2014from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language\u2014and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement a variety of arithmetic and geometric operators that are building blocks for important oracles, including those used in Shor\u2019s and Grover\u2019s algorithms. We found that VQO\u2019s QFT-based arithmetic oracles require fewer qubits, sometimes substantially fewer, than those constructed using \u201cclassical\u201d gates; VQO\u2019s versions of the latter were nevertheless on par with or better than (in terms of both qubit and gate counts) oracles produced by Quipper, a state-of-the-art but unverified quantum programming platform.<\/jats:p>","DOI":"10.1145\/3563309","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"589-615","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Verified compilation of Quantum oracles"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-0244","authenticated-orcid":false,"given":"Liyi","family":"Li","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1913-4178","authenticated-orcid":false,"given":"Finn","family":"Voichick","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2724-0974","authenticated-orcid":false,"given":"Kesha","family":"Hietala","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0592-7131","authenticated-orcid":false,"given":"Yuxiang","family":"Peng","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8877-9802","authenticated-orcid":false,"given":"Xiaodi","family":"Wu","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2759-9223","authenticated-orcid":false,"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland, USA \/ Amazon, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, Frederic Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun.","author":"Abhari Ali","year":"2012","unstructured":"Ali Abhari , Arvin Faruque , Mohammad Javad Dousti , Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, Frederic Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun. 2012 . Scaffold : Quantum Programming Language. Princeton University . Ali Abhari, Arvin Faruque, Mohammad Javad Dousti, Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, Frederic Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun. 2012. Scaffold: Quantum Programming Language. Princeton University."},{"key":"e_1_2_1_2_1","volume-title":"Svore","author":"Amy Matthew","year":"2017","unstructured":"Matthew Amy , Martin Roetteler , and Krysta M . Svore . 2017 . Verified Compilation of Space-Efficient Reversible Circuits. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing , Cham. 3\u201321. isbn:978-3-319-63390-9 Matthew Amy, Martin Roetteler, and Krysta M. Svore. 2017. Verified Compilation of Space-Efficient Reversible Circuits. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 3\u201321. isbn:978-3-319-63390-9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1103\/physreva.54.139"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.26421\/QIC3.2-8"},{"key":"e_1_2_1_5_1","unstructured":"Daniel J. Bernstein. 2008. ChaCha a variant of Salsa20. The State of the Art of Stream Ciphers. ECRYPT Network of Excellence in Cryptology 273\u2013278. https:\/\/cr.yp.to\/papers.html##chacha Daniel J. Bernstein. 2008. ChaCha a variant of Salsa20. The State of the Art of Stream Ciphers. ECRYPT Network of Excellence in Cryptology 273\u2013278. https:\/\/cr.yp.to\/papers.html##chacha"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12929-2_6"},{"key":"e_1_2_1_7_1","volume-title":"Compile Quipper quantum circuit to OpenQasm 2.0 program. https:\/\/www.mathstat.dal.ca\/~xbian\/QasmTrans\/ [Online","author":"Bian Xiaoning","year":"2021","unstructured":"Xiaoning Bian . 2020. Compile Quipper quantum circuit to OpenQasm 2.0 program. https:\/\/www.mathstat.dal.ca\/~xbian\/QasmTrans\/ [Online ; accessed 8- July - 2021 ] Xiaoning Bian. 2020. Compile Quipper quantum circuit to OpenQasm 2.0 program. https:\/\/www.mathstat.dal.ca\/~xbian\/QasmTrans\/ [Online; accessed 8-July-2021]"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"#cr-split#-e_1_2_1_9_1.1","unstructured":"Lukas Burgholzer Hartwig Bauer and Robert Wille. 2021. Hybrid Schr\u00f6dinger-Feynman Simulation of Quantum Circuits With Decision Diagrams. https:\/\/doi.org\/10.48550\/ARXIV.2105.07045 arxiv:2105.07045. 10.48550\/ARXIV.2105.07045"},{"key":"#cr-split#-e_1_2_1_9_1.2","doi-asserted-by":"crossref","unstructured":"Lukas Burgholzer Hartwig Bauer and Robert Wille. 2021. Hybrid Schr\u00f6dinger-Feynman Simulation of Quantum Circuits With Decision Diagrams. https:\/\/doi.org\/10.48550\/ARXIV.2105.07045 arxiv:2105.07045.","DOI":"10.1109\/QCE52317.2021.00037"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00220-009-0930-1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_13_1","volume-title":"APS Meeting Abstracts.","author":"Cross Andrew","year":"2018","unstructured":"Andrew Cross . 2018 . The IBM Q experience and QISKit open-source quantum computing software . In APS Meeting Abstracts. Andrew Cross. 2018. The IBM Q experience and QISKit open-source quantum computing software. In APS Meeting Abstracts."},{"key":"e_1_2_1_14_1","volume-title":"Gambetta","author":"Cross Andrew W.","year":"2017","unstructured":"Andrew W. Cross , Lev S. Bishop , John A. Smolin , and Jay M . Gambetta . 2017 . Open quantum assembly language. arXiv e-prints, Jul, https:\/\/doi.org\/10.48550\/ARXIV.1707.03429 arxiv:1707.03429. 10.48550\/ARXIV.1707.03429 Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. 2017. Open quantum assembly language. arXiv e-prints, Jul, https:\/\/doi.org\/10.48550\/ARXIV.1707.03429 arxiv:1707.03429."},{"key":"#cr-split#-e_1_2_1_15_1.1","unstructured":"Thomas G. Draper. 2000. Addition on a Quantum Computer. arXiv e-prints Article quant-ph\/0008033 Aug. quant-ph\/0008033 pages. https:\/\/doi.org\/10.48550\/ARXIV.QUANT-PH\/0008033 arxiv:quant-ph\/0008033. 10.48550\/ARXIV.QUANT-PH"},{"key":"#cr-split#-e_1_2_1_15_1.2","unstructured":"Thomas G. Draper. 2000. Addition on a Quantum Computer. arXiv e-prints Article quant-ph\/0008033 Aug. quant-ph\/0008033 pages. https:\/\/doi.org\/10.48550\/ARXIV.QUANT-PH\/0008033 arxiv:quant-ph\/0008033."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02650179"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2021-04-15-433"},{"key":"e_1_2_1_18_1","volume-title":"Cirq: An Open Source Framework for Programming Quantum Computers. https:\/\/quantumai.google\/cirq","author":"Google Quantum","year":"2019","unstructured":"Google Quantum AI. 2019 . Cirq: An Open Source Framework for Programming Quantum Computers. https:\/\/quantumai.google\/cirq Google Quantum AI. 2019. Cirq: An Open Source Framework for Programming Quantum Computers. https:\/\/quantumai.google\/cirq"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.79.325"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2000.892139"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.21"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_2_1_25_1","unstructured":"N.D. Jones C.K. Gomard and P. Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice Hall. isbn:9780130202499 lccn:lc93016674 https:\/\/books.google.com\/books?id=7rPPScYo8w8C N.D. Jones C.K. Gomard and P. Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice Hall. isbn:9780130202499 lccn:lc93016674 https:\/\/books.google.com\/books?id=7rPPScYo8w8C"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7905"},{"key":"#cr-split#-e_1_2_1_27_1.1","unstructured":"Liyi Li Finn Voichick Kesha Hietala Yuxiang Peng Xiaodi Wu and Michael Hicks. 2021. Verified Compilation of Quantum Oracles. https:\/\/doi.org\/10.48550\/ARXIV.2112.06700 10.48550\/ARXIV.2112.06700"},{"key":"#cr-split#-e_1_2_1_27_1.2","doi-asserted-by":"crossref","unstructured":"Liyi Li Finn Voichick Kesha Hietala Yuxiang Peng Xiaodi Wu and Michael Hicks. 2021. Verified Compilation of Quantum Oracles. https:\/\/doi.org\/10.48550\/ARXIV.2112.06700","DOI":"10.1145\/3563309"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7068972"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab8c2c"},{"key":"e_1_2_1_30_1","first-page":"5","article-title":"Constant-Optimized Quantum Circuits for Modular Multiplication and Exponentiation. Quantum Info","volume":"12","author":"Markov Igor L.","year":"2012","unstructured":"Igor L. Markov and Mehdi Saeedi . 2012 . Constant-Optimized Quantum Circuits for Modular Multiplication and Exponentiation. Quantum Info . Comput. , 12 , 5 \u2013 6 (2012), May, 361\u2013394. issn:1533-7146 Igor L. Markov and Mehdi Saeedi. 2012. Constant-Optimized Quantum Circuits for Modular Multiplication and Exponentiation. Quantum Info. Comput., 12, 5\u20136 (2012), May, 361\u2013394. issn:1533-7146","journal-title":"Comput."},{"key":"e_1_2_1_31_1","unstructured":"Microsoft. 2017. The Q# Programming Language. https:\/\/docs.microsoft.com\/ Microsoft. 2017. The Q# Programming Language. https:\/\/docs.microsoft.com\/"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41534-020-0257-5"},{"key":"e_1_2_1_33_1","volume-title":"Chuang","author":"Nielsen Michael A.","year":"2011","unstructured":"Michael A. Nielsen and Isaac L . Chuang . 2011 . Quantum Computation and Quantum Information (10th anniversary ed.). Cambridge University Press , USA. isbn:1107002176 Michael A. Nielsen and Isaac L. Chuang. 2011. Quantum Computation and Quantum Information (10th anniversary ed.). Cambridge University Press, USA. isbn:1107002176"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454040"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"#cr-split#-e_1_2_1_36_1.1","unstructured":"Yuxiang Peng Kesha Hietala Runzhou Tao Liyi Li Robert Rand Michael Hicks and Xiaodi Wu. 2022. A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm. https:\/\/doi.org\/10.48550\/ARXIV.2204.07112 10.48550\/ARXIV.2204.07112"},{"key":"#cr-split#-e_1_2_1_36_1.2","unstructured":"Yuxiang Peng Kesha Hietala Runzhou Tao Liyi Li Robert Rand Michael Hicks and Xiaodi Wu. 2022. A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm. https:\/\/doi.org\/10.48550\/ARXIV.2204.07112"},{"key":"e_1_2_1_37_1","volume-title":"Formally verified quantum programming. Ph. D. Dissertation","author":"Rand Robert","unstructured":"Robert Rand . 2018. Formally verified quantum programming. Ph. D. Dissertation . University of Pennsylvania . Robert Rand. 2018. Formally verified quantum programming. Ph. D. Dissertation. University of Pennsylvania."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.287.17"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC8446"},{"key":"e_1_2_1_40_1","unstructured":"Rigetti Computing. 2019. The @rigetti optimizing Quil compiler. https:\/\/github.com\/rigetti\/quilc Rigetti Computing. 2019. The @rigetti optimizing Quil compiler. https:\/\/github.com\/rigetti\/quilc"},{"key":"e_1_2_1_41_1","unstructured":"Rigetti Computing. 2021. PyQuil: Quantum programming in Python. https:\/\/pyquil-docs.rigetti.com Rigetti Computing. 2021. PyQuil: Quantum programming in Python. https:\/\/pyquil-docs.rigetti.com"},{"key":"e_1_2_1_42_1","unstructured":"Yunong Shi Xupeng Li Runzhou Tao Ali Javadi-Abhari Andrew W. Cross Frederic T. Chong and Ronghui Gu. 2019. Contract-based verification of a realistic quantum compiler. arXiv e-prints Aug arxiv:1908.08963. Yunong Shi Xupeng Li Runzhou Tao Ali Javadi-Abhari Andrew W. Cross Frederic T. Chong and Ronghui Gu. 2019. Contract-based verification of a realistic quantum compiler. arXiv e-prints Aug arxiv:1908.08963."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Rolando Somma. 2020. Are We Ready for Quantum Computers? Scientific American https:\/\/blogs.scientificamerican.com\/observations\/are-we-ready-for-quantum-computers Rolando Somma. 2020. Are We Ready for Quantum Computers? Scientific American https:\/\/blogs.scientificamerican.com\/observations\/are-we-ready-for-quantum-computers","DOI":"10.1038\/scientificamerican062020-7N0voCA2cqSLmQ6FagVcko"},{"key":"e_1_2_1_45_1","volume-title":"The Way I See It: The State of Quantum Computing","author":"Wilkins Angela","year":"2021","unstructured":"Angela Wilkins . 2021. The Way I See It: The State of Quantum Computing . Rice University , https:\/\/news.rice.edu\/news\/ 2021 \/way-i-see-it-state-quantum-computing Angela Wilkins. 2021. The Way I See It: The State of Quantum Computing. Rice University, https:\/\/news.rice.edu\/news\/2021\/way-i-see-it-state-quantum-computing"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563309","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563309","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563309","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563309"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":49,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563309"],"URL":"https:\/\/doi.org\/10.1145\/3563309","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}