{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:36Z","timestamp":1780994616212,"version":"3.54.1"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            Quantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. Automated tools relieving the tedium and errors associated with low-level quantum details would hence be highly desirable. In this paper, we initiate the study of\n            <jats:italic toggle=\"yes\">program synthesis<\/jats:italic>\n            for quantum unitary programs that recursively define a family of unitary circuits for different input sizes, which are widely used in existing quantum programming languages. Specifically, we present QSynth, the first quantum program synthesis framework, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes 10 quantum unitary programs including quantum arithmetic programs, quantum eigenvalue inversion, quantum teleportation and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.\n          <\/jats:p>","DOI":"10.1145\/3632901","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1759-1788","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["A Case for Synthesis of Recursive Quantum Unitary Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3616-9337","authenticated-orcid":false,"given":"Haowei","family":"Deng","sequence":"first","affiliation":[{"name":"University of Maryland, College Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3733-5168","authenticated-orcid":false,"given":"Runzhou","family":"Tao","sequence":"additional","affiliation":[{"name":"Columbia University, New York, 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, College Park, 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, College Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Matthew Amy. 2018. Towards large-scale functional verification of universal quantum circuits. arXiv preprint arXiv:1805.06908 (2018). https:\/\/doi.org\/10.4204\/eptcs.287.1 10.4204\/eptcs.287.1","DOI":"10.4204\/eptcs.287.1"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aad8ca"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2341953"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2013.2244643"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.2019.2906374"},{"key":"e_1_3_1_9_1","unstructured":"Dave Bacon Wim van Dam and Alexander Russell. 2008. Analyzing algebraic quantum circuits using exponential sums. unpublished: see tinyurl. com\/qpo7s2 (2008)."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539796300921"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.116.250501"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Christophe Chareton Sbastien Bardin Franccois Bobot Valentin Perrelle and Benoit Valiron. 2020. A Deductive Verification Framework for Circuit-building Quantum Programs. arXiv preprint arXiv:2003.05841 (2020). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_6 10.1007\/978-3-030-72019-3_6","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_1_16_1","unstructured":"Don Coppersmith. 2002. An approximate Fourier transform useful in quantum factoring. arXiv preprint quant-ph\/0201067 (2002)."},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Steven A Cuccaro Thomas G Draper Samuel A Kutin and David Petrie Moulton. 2004. A new quantum ripple-carry addition circuit. arXiv preprint quant-ph\/0410184 (2004). https:\/\/doi.org\/10.48550\/arXiv.quant-ph\/0410184 10.48550\/arXiv.quant-ph\/0410184","DOI":"10.48550\/arXiv.quant-ph\/0410184"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Christopher M Dawson and Michael A Nielsen. 2005. The solovay-kitaev algorithm. arXiv preprint quant-ph\/0505030 (2005). https:\/\/doi.org\/10.26421\/QIC6.1-6 10.26421\/QIC6.1-6","DOI":"10.26421\/QIC6.1-6"},{"key":"e_1_3_1_19_1","volume-title":"Methods for optimizing the synthesis of quantum circuits","author":"Brugiere Timothee Goubault de","year":"2020","unstructured":"Timothee Goubault de Brugiere. 2020. Methods for optimizing the synthesis of quantum circuits. Ph. D. Dissertation. Universite Paris-Saclay."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579369"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Haowei Deng Zhoutao Run Yuxiang Peng and Xiaodi Wu. 2023b. QSynth Zenodo. (2023). https:\/\/doi.org\/10.5281\/zenodo.10054966 10.5281\/zenodo.10054966","DOI":"10.5281\/zenodo.10054966"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1992.0167"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Menghan Dou Tianrui Zou Yuan Fang Jing Wang Dongyi Zhao Lei Yu Boying Chen Wenbo Guo Ye Li Zhaoyun Chen et al. 2022. QPanda: high-performance quantum computing framework for multiple application scenarios. arXiv preprint arXiv:2212.14201 (2022). https:\/\/doi.org\/10.48550\/arXiv.2212.14201 10.48550\/arXiv.2212.14201","DOI":"10.48550\/arXiv.2212.14201"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_4"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Mark Ettinger and Peter Hoyer. 1999. A quantum observable for the graph isomorphism problem. arXiv preprint quant-ph\/9901029 (1999). https:\/\/doi.org\/10.48550\/arXiv.quant-ph\/9901029 10.48550\/arXiv.quant-ph\/9901029","DOI":"10.48550\/arXiv.quant-ph\/9901029"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Yu Feng Ruben Martins Yuepeng Wang Isil Dillig and Thomas W Reps. 2017. Component-based synthesis for complex APIs. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 599\u2013612. https:\/\/doi.org\/10.1145\/3009837.3009851 10.1145\/3009837.3009851","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01886518"},{"key":"e_1_3_1_28_1","unstructured":"Jay Gambetta. 2022. IBM Quantum Roadmap to build quantum-centric supercomputers. https:\/\/research.ibm.com\/blog\/ibm-quantum-roadmap-2025"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Daniel M Greenberger Michael A Horne and Anton Zeilinger. 1989. Going beyond Bell\u2019s theorem. (1989) 69\u201372. https:\/\/doi.org\/10.1007\/978-94-017-0849-4_10 10.1007\/978-94-017-0849-4_10","DOI":"10.1007\/978-94-017-0849-4_10"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240260"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993505"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.59.1829"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_37"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_21"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586039"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"A Yu Kitaev. 1995. Quantum measurements and the Abelian stabilizer problem. arXiv preprint quant-ph\/9511026 (1995). https:\/\/doi.org\/10.48550\/arXiv.quant-ph\/9511026 10.48550\/arXiv.quant-ph\/9511026","DOI":"10.48550\/arXiv.quant-ph\/9511026"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1070\/RM1997v052n06ABEH002155"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11931-6_3"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Tristan Knoth Di Wang Nadia Polikarpova and Jan Hoffmann. 2019. Resource-guided program synthesis. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 253\u2013268. https:\/\/doi.org\/10.1145\/3314221.3314602 10.1145\/3314221.3314602","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Dax Enshan Koh Mark D Penney and Robert W Spekkens. 2017. Computing quopit Clifford circuit amplitudes by the sum-over-paths technique. Quantum Information & Computation (2017). https:\/\/doi.org\/10.26421\/QIC17.13-14-1 10.26421\/QIC17.13-14-1","DOI":"10.26421\/QIC17.13-14-1"},{"key":"e_1_3_1_46_1","unstructured":"Percy Liang Michael I Jordan and Dan Klein. 2010. Learning programs: A hierarchical Bayesian approach. In Proceedings of the 27th International Conference on Machine Learning (ICML-10). 639\u2013646."},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11128-014-0779-x"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629430"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_1_50_1","unstructured":"Aditya Menon Omer Tamuz Sumit Gulwani Butler Lampson and Adam Kalai. 2013. A machine learning framework for programming by example. In International Conference on Machine Learning. PMLR 187\u2013195."},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1088\/1751-8121\/aa565f"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","unstructured":"Phitchaya Mangpo Phothilimthana Aditya Thakur Rastislav Bodik and Dinakar Dhurjati. 2016. Scaling up superoptimization. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems. 297\u2013310. https:\/\/doi.org\/10.1145\/2872362.2872387 10.1145\/2872362.2872387","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"Oleksandr Polozov and Sumit Gulwani. 2015. Flashmeta: A framework for inductive program synthesis. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications. 107\u2013126. https:\/\/doi.org\/10.1145\/2858965.2814310 10.1145\/2858965.2814310","DOI":"10.1145\/2858965.2814310"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11128-010-0201-2"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.855930"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","unstructured":"Peter W Shor. 1994. Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings 35th annual symposium on foundations of computer science. Ieee 124\u2013134. https:\/\/doi.org\/10.1109\/SFCS.1994.365700 10.1109\/SFCS.1994.365700","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_1_59_1","volume-title":"Program synthesis by sketching","author":"Solar-Lezama Armando","year":"2008","unstructured":"Armando Solar-Lezama. 2008. Program synthesis by sketching. University of California, Berkeley."},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","unstructured":"Runzhou Tao Yunong Shi Jianan Yao Xupeng Li Ali Javadi-Abhari Andrew W Cross Frederic T Chong and Ronghui Gu. 2022. Giallar: push-button verification for the qiskit Quantum compiler. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 641\u2013656. https:\/\/doi.org\/10.1145\/3519939.3523431 10.1145\/3519939.3523431","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/iNIS.2017.34"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bodik. 2013. Growing solver-aided languages with Rosette. In Proceedings of the 2013 ACM international symposium on New ideas new paradigms and reflections on programming & software. 135\u2013152. https:\/\/doi.org\/10.1145\/2509578.2509586 10.1145\/2509578.2509586","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","unstructured":"Yan Xia Chang-Bao Fu Shou Zhang Suc-Kyoung Hong Kyu-Hwang Yeon and Chung-In Um. 2006. Quantum dialogue by using the GHZ state. arXiv preprint quant-ph\/0601127 (2006). https:\/\/doi.org\/10.48550\/arXiv.quant-ph\/0601127 10.48550\/arXiv.quant-ph\/0601127","DOI":"10.48550\/arXiv.quant-ph\/0601127"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","unstructured":"Amanda Xu Abtin Molavi Lauren Pick Swamit Tannu and Aws Albarghouthi. 2023. Synthesizing Quantum-Circuit Optimizers. Proceedings of the ACM on Programming Languages 7 PLDI (2023) 835\u2013859. https:\/\/doi.org\/10.1145\/3591254 10.1145\/3591254","DOI":"10.1145\/3591254"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","unstructured":"Mingkuan Xu Zikun Li Oded Padon Sina Lin Jessica Pointing Auguste Hirth Henry Ma Jens Palsberg Alex Aiken Umut A Acar et al. 2022. Quartz: superoptimization of Quantum circuits. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 625\u2013640. https:\/\/doi.org\/10.1145\/3519939.3523433 10.1145\/3519939.3523433","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","unstructured":"Ed Younis Koushik Sen Katherine Yelick and Costin Iancu. 2021. Qfast: Conflating search and numerical optimization for scalable quantum circuit synthesis. In 2021 IEEE International Conference on Quantum Computing and Engineering (QCE). IEEE 232\u2013243. https:\/\/doi.org\/10.1109\/QCE52317.2021.00041 10.1109\/QCE52317.2021.00041","DOI":"10.1109\/QCE52317.2021.00041"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","unstructured":"Nengkun Yu and Jens Palsberg. 2021. Quantum abstract interpretation. In Proceedings ofthe 42ndACM SIGPLAN International Conference on Programming Language Design and Implementation. 542\u2013558. https:\/\/doi.org\/10.1145\/3453483.3454061 10.1145\/3453483.3454061","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1088\/0256-307X\/23\/7\/007"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632901","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632901","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:40Z","timestamp":1751659360000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632901"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":68,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632901"],"URL":"https:\/\/doi.org\/10.1145\/3632901","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}