{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:37:48Z","timestamp":1773193068768,"version":"3.50.1"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Ministry of Education and Science of Bulgaria","award":["Bulgarian National Roadmap for Research Infrastructure"],"award-info":[{"award-number":["Bulgarian National Roadmap for Research Infrastructure"]}]},{"DOI":"10.13039\/501100001711","name":"SNSF","doi-asserted-by":"crossref","award":["207967"],"award-info":[{"award-number":["207967"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>A key challenge of quantum programming is uncomputation: the reversible deallocation of qubits. And while there has been much recent progress on automating uncomputation, state-of-the-art methods are insufficient for handling today's expressive quantum programming languages. A core reason is that they operate on primitive quantum circuits, while quantum programs express computations beyond circuits, for instance, they can capture families of circuits defined recursively in terms of uncomputation and adjoints.<\/jats:p>\n                  <jats:p>In this paper, we introduce the first modular automatic approach to synthesize correct and efficient uncomputation for expressive quantum programs. Our method is based on two core technical contributions: (i) an intermediate representation (IR) that can capture expressive quantum programs and comes with support for uncomputation, and (ii) modular algorithms over that IR for synthesizing uncomputation and adjoints.<\/jats:p>\n                  <jats:p>We have built a complete end-to-end implementation of our method, including an implementation of the IR and the synthesis algorithms, as well as a translation from an expressive fragment of the Silq programming language to our IR and circuit generation from the IR. Our experimental evaluation demonstrates that we can handle programs beyond the capabilities of existing uncomputation approaches, while being competitive on the benchmarks they can handle. More broadly, we show that it is possible to benefit from the greater expressivity and safety offered by high-level quantum languages without sacrificing efficiency.<\/jats:p>","DOI":"10.1145\/3689785","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2097-2124","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Modular Synthesis of Efficient Quantum Uncomputation"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-5394-4340","authenticated-orcid":false,"given":"Hristo","family":"Venev","sequence":"first","affiliation":[{"name":"Sofia University St. Kliment Ohridski, Sofia, Bulgaria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7470-0489","authenticated-orcid":false,"given":"Timon","family":"Gehr","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9393-0925","authenticated-orcid":false,"given":"Dimitar","family":"Dimitrov","sequence":"additional","affiliation":[{"name":"Sofia University St. Kliment Ohridski, Sofia, Bulgaria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0054-9568","authenticated-orcid":false,"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"},{"name":"Sofia University St. Kliment Ohridski, Sofia, Bulgaria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Gadi Aleksandrowicz Thomas Alexander Panagiotis Barkoutsos Luciano Bello Yael Ben-Haim David Bucher Francisco Jose Cabrera-Hern\u00e1ndez Jorge Carballo-Franquis Adrian Chen Chun-Fu Chen Jerry M. Chow Antonio D. C\u00f3rcoles-Gonzales Abigail J. Cross Andrew Cross Juan Cruz-Benito Chris Culver Salvador De La Puente Gonz\u00e1lez Enrique De La Torre Delton Ding Eugene Dumitrescu Ivan Duran Pieter Eendebak Mark Everitt Ismael Faro Sertage Albert Frisch Andreas Fuhrer Jay Gambetta Borja Godoy Gago Juan Gomez-Mosquera Donny Greenberg Ikko Hamamura Vojtech Havlicek Joe Hellmers Lukasz Herok Hiroshi Horii Shaohan Hu Takashi Imamichi Toshinari Itoko Ali Javadi-Abhari Naoki Kanazawa Anton Karazeev Kevin Krsulich Peng Liu Yang Luh Yunho Maeng Manoel Marques Francisco Jose Mart\u00edn-Fern\u00e1ndez Douglas T. McClure David McKay Srujan Meesala Antonio Mezzacapo Nikolaj Moll Diego Moreda Rodr\u00edguez Giacomo Nannicini Paul Nation Pauline Ollitrault Lee James O'Riordan Hanhee Paik Jes\u00fas P\u00e9rez Anna Phan Marco Pistoia Viktor Prutyanov Max Reuter Julia Rice Abd\u00f3n Rodr\u00edguez Davila Raymond Harry Putra Rudy Mingi Ryu Ninad Sathaye Chris Schnabel Eddie Schoute Kanav Setia Yunong Shi Adenilton Silva Yukio Siraichi Seyon Sivarajah John A. Smolin Mathias Soeken Hitomi Takahashi Ivano Tavernelli Charles Taylor Pete Taylour Kenso Trabing Matthew Treinish Wes Turner Desiree Vogt-Lee Christophe Vuillot Jonathan A. Wildstrom Jessica Wilson Erick Winston Christopher Wood Stephen Wood Stefan Worner Ismail Yunus Akhalwaya and Christa Zoufal. 2019. Qiskit: An Open-source Framework for Quantum Computing. https:\/\/doi.org\/10.5281\/zenodo.2562111 10.5281\/zenodo.2562111","DOI":"10.5281\/zenodo.2562111"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"T. Altenkirch and J. Grattage. 2005. A functional quantum programming language. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05). 249-258. https:\/\/doi.org\/10.1109\/LICS.2005.1 10.1109\/LICS.2005.1 ISSN: 1043-6871.","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_3_2_5_1","first-page":"3","volume-title":"International Conference on Computer Aided Verification","author":"Amy Matthew","year":"2017","unstructured":"Matthew Amy, Martin Roetteler, and Krysta M Svore. 2017. Verified compilation of space-efficient reversible circuits. In International Conference on Computer Aided Verification. Springer, 3\u201321."},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.176.0525"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/0218053"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.70.1895"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_3_2_10_1","unstructured":"Alan Davis and Robert Keller. 1982. Data Flow Program Graphs. All HMC Faculty Publications and Research (Feb. 1982). https:\/\/scholarship.claremont.edu\/hmc_fac_pub\/285"},{"key":"e_1_3_2_11_1","first-page":"153","volume-title":"Reversible Computation: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings 12","author":"Fu Peng","year":"2020","unstructured":"Peng Fu, Kohei Kishida, Neil J Ross, and Peter Selinger 2020. A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper. In Reversible Computation: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings 12, Springer, 153\u2013168."},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57659-2_28"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498663"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3491247"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103667"},{"key":"e_1_3_2_17_1","unstructured":"Yves Lecerf. 1963. Machines de Turing r\u00e9versibles. R\u00e9cursive insolubilit\u00e9 en n g N de l\u2018\u00e9quation u = 6nu o\u00f9 6 est un isomorphisme de codes. Comptes Rendus Hebdomadaires des Seances de L'academie des Sciences 257 (1963) 2597-2600."},{"key":"e_1_3_2_18_1","unstructured":"Microsoft. 2020. Q# Language Specification. Retrieved Jul 7 2023 from https:\/\/github.com\/microsoft\/qsharp-language\/tree\/main\/Specifications\/Language#q-language"},{"key":"e_1_3_2_19_1","volume-title":"Quantum Computation and Quantum Information: 10th Anniversary Edition","author":"Nielsen Michael A.","year":"2020","unstructured":"Michael A. Nielsen and Isaac L. Chuang. 2020. Quantum Computation and Quantum Information: 10th Anniversary Edition, Cambridge University Press."},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/93548.93578"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454040"},{"key":"e_1_3_2_22_1","doi-asserted-by":"crossref","unstructured":"Anouk Paradis Benjamin Bichsel and Martin Vechev. 2022. Reqomp: Space-constrained Uncomputation for Quantum Circuits. arXiv:2212.10395 [quant-ph]","DOI":"10.1145\/3453483.3454040"},{"key":"e_1_3_2_23_1","unstructured":"Alex Parent Martin Roetteler and Krysta M. Svore. 2015. Reversible circuit compilation with space constraints. CoRR abs\/1510.00377 (2015). arXiv:1510.00377 http:\/\/arxiv.org\/abs\/1510.00377"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497776.3517772"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/s0097539795293172"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10003-2_104"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Hristo Venev Timon Gehr Dimitar Dimitrov and Martin Vechev. 2024. Artifact for \u201cModular Synthesis of Efficient Quantum Uncomputation\u201d. https:\/\/doi.org\/10.5281\/zenodo.13487216 10.5281\/zenodo.13487216","DOI":"10.5281\/zenodo.13487216"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571225"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563297"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689785","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689785","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:10:20Z","timestamp":1770196220000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689785"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":30,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689785"],"URL":"https:\/\/doi.org\/10.1145\/3689785","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}