{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:10Z","timestamp":1767929650905,"version":"3.49.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/X025551\/1"],"award-info":[{"award-number":["EP\/X025551\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000183","name":"U.S. Army Research Office","doi-asserted-by":"crossref","award":["W911NF-23-1-0045"],"award-info":[{"award-number":["W911NF-23-1-0045"]}],"id":[{"id":"10.13039\/100000183","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":[[2026,1,8]]},"abstract":"<jats:p>Quantum programs today are written at a low level of abstraction - quantum circuits akin to assembly languages - and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed.<\/jats:p>\n                  <jats:p>To this end, we introduce a simple syntax for generating unitaries from \"just a phase\"; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the \"if let\" construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design.<\/jats:p>\n                  <jats:p>We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover's search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.<\/jats:p>","DOI":"10.1145\/3776731","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2586-2613","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Quantum Circuits Are Just a Phase"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7393-2640","authenticated-orcid":false,"given":"Chris","family":"Heunen","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1761-3244","authenticated-orcid":false,"given":"Louis","family":"Lemonnier","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4927-0613","authenticated-orcid":false,"given":"Christopher","family":"McNally","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2698-5122","authenticated-orcid":false,"given":"Alex","family":"Rice","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1002\/9781444340563"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932506"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"T. Altenkirch and J. Grattage. 2005. A Functional Quantum Programming Language. In Logic in Computer Science. IEEE 249\u2013258. https:\/\/doi.org\/10.1109\/LICS.2005.1 10.1109\/LICS.2005.1","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ac47f1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"B. Bichsel M. Baader T. Gehr and M. Vechev. 2020. Silq: A high-level quantum language with safe uncomputation and intuitive semantics. In Programming Language Design and Implementation. ACM 286\u2013300. https:\/\/doi.org\/10.1145\/3385412.3386007 10.1145\/3385412.3386007","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.94.022340"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"N. Bot\u00f6 and F. Forslund. 2023. The zeta calculus. (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.17399 arXiv:2303.17399. 10.48550\/arXiv.2303.17399","DOI":"10.48550\/arXiv.2303.17399"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"K. R. Brown A. W. Harrow and I. L. Chuang. 2004. Arbitrarily accurate composite pulse sequences. Physical Review A\u2014Atomic Molecular and Optical Physics 70 5 (2004) 052318. https:\/\/doi.org\/10.1103\/PhysRevA.70.052318 10.1103\/PhysRevA.70.052318","DOI":"10.1103\/PhysRevA.70.052318"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.195.3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632861"},{"key":"e_1_2_1_11_1","unstructured":"K. Chardonnet. 2023. Towards a Curry-Howard Correspondence for Quantum Computation. Ph. D. Dissertation. Universit\u00e9 Paris-Saclay. https:\/\/theses.hal.science\/tel-03959403"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2024.19"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.88.022318"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175801"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_25"},{"key":"e_1_2_1_16_1","unstructured":"McKinsey & Company. 2024. Quantum Technology Monitor. Digital. https:\/\/www.mckinsey.com\/~\/media\/mckinsey\/business"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505636"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"K. Dave L. Lemonnier R. P\u00e9choux and V. Zamdzhiev. 2025. Combining quantum and classical control: syntax semantics and adequacy. In Foundations of Software Science and Computation Structures. Springer 155\u2013175. isbn:978-3-031-90897-2 https:\/\/doi.org\/10.1007\/978-3-031-90897-2_8 10.1007\/978-3-031-90897-2_8","DOI":"10.1007\/978-3-031-90897-2_8"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2022.119"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"M. Di Meglio. 2023. Pre-Hilbert *-categories: the Hilbert-space analogue of abelian categories. (2023). https:\/\/doi.org\/10.48550\/arXiv.2312.02883 arXiv:2313.02883. 10.48550\/arXiv.2312.02883","DOI":"10.48550\/arXiv.2312.02883"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-95908-0_3"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41467-017-01904-7"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571204"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"P. Fu K. Kishida N. J. Ross and P. Selinger. 2024. Proto-Quipper with Reversing and Control. arxiv:2410.22261 [cs] https:\/\/doi.org\/10.48550\/arXiv.2410.22261 10.48550\/arXiv.2410.22261","DOI":"10.48550\/arXiv.2410.22261"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1038\/s42254-020-00245-7"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498663"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.2117024119"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1112\/blms.13010"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"C. Heunen and J. Vicary. 2019. Categories for Quantum Theory: an introduction. Oxford University Press. https:\/\/doi.org\/10.1093\/oso\/9780198739623.001.0001 10.1093\/oso\/9780198739623.001.0001","DOI":"10.1093\/oso\/9780198739623.001.0001"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704842"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076450.2076469"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656436"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.08.003"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.351.10"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"T. Khattar and C. Gidney. 2025. Rise of conditionally clean ancillae for efficient quantum circuit constructions. Quantum 9 (May 2025) 1752. issn:2521-327X https:\/\/doi.org\/10.22331\/q-2025-05-21-1752 10.22331\/q-2025-05-21-1752","DOI":"10.22331\/q-2025-05-21-1752"},{"key":"e_1_2_1_37_1","unstructured":"S. Klabnik and C. Nichols. 2023. The Rust programming language. No Starch Press."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059555"},{"key":"e_1_2_1_39_1","unstructured":"L. Lemonnier. 2024. The Semantics of Effects: Centrality Quantum Control and Reversible Recursion. Ph. D. Dissertation. Universit\u00e9 Paris-Saclay. https:\/\/theses.hal.science\/tel-04625771"},{"key":"e_1_2_1_40_1","volume-title":"Universal quantum simulators. Science 273, 5278","author":"Lloyd S.","year":"1996","unstructured":"S. Lloyd. 1996. Universal quantum simulators. Science 273, 5278 (1996), 1073\u20131078. https:\/\/doi.org\/Universal quantum simulators"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"G. H. Low and I. L. Chuang. 2017. Optimal Hamiltonian simulation by quantum signal processing. Physical review letters 118 1 (2017) 010501. https:\/\/doi.org\/10.1103\/PhysRevLett.118.010501 10.1103\/PhysRevLett.118.010501","DOI":"10.1103\/PhysRevLett.118.010501"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"G. H. Low and Y. Su. 2024. Quantum eigenvalue processing. In Foundations of Computer Science (FOCS). IEEE 1051\u20131062. https:\/\/doi.org\/10.1109\/FOCS61266.2024.00070 10.1109\/FOCS61266.2024.00070","DOI":"10.1109\/FOCS61266.2024.00070"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevX.6.041067"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1103\/PRXQuantum.2.040203"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"M. Di Meglio C. Heunen J-S. P. Lemay P. Perrone and D. Stein. 2025. Dagger categories of relations: the equivalence of dilatory dagger categories and epi-regular independence categories. (2025). https:\/\/doi.org\/10.48550\/arXiv.2508.01146 arXiv:2508.01146. 10.48550\/arXiv.2508.01146","DOI":"10.48550\/arXiv.2508.01146"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"M. A. Nielsen and I. L. Chuang. 2010. Quantum Computation and Quantum Information (10th anniversary edition ed.). Cambridge university press. isbn:978-1-107-00217-3 https:\/\/doi.org\/10.1017\/CBO9780511976667 10.1017\/CBO9780511976667","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","unstructured":"M. Pagani P. Selinger and B. Valiron. 2014. Applying quantitative semantics to higher-order quantum computing. In Principles of Programming Languages. ACM 647\u2013658. https:\/\/doi.org\/10.1145\/2535838.2535879 10.1145\/2535838.2535879","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1038\/ncomms8913"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","unstructured":"A. Rice. 2025. Phase-rs - rust implementation of quantum phase language. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.17467011 10.5281\/zenodo.17467011","DOI":"10.5281\/zenodo.17467011"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_19"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"J. J. Sakurai and J. Napolitano. 2020. Modern quantum mechanics. Cambridge University Press.","DOI":"10.1017\/9781108587280"},{"key":"e_1_2_1_52_1","unstructured":"P. Selinger. 2004. Towards a semantics for higher-order quantum computation. In Quantum Physics and Logic. 127\u2013143."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503224"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.2307\/2033649"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100790"},{"key":"e_1_2_1_57_1","unstructured":"B. Valiron. 2024. On Quantum Programming Languages. HDR. Universit\u00e9 Paris Saclay. https:\/\/theses.hal.science\/tel-04740855"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699415"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571225"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","unstructured":"W. Wootters and W. Zurek. 1982. A single quantum cannot be cloned. Nature 299 5886 (1982) 802\u2013803. https:\/\/doi.org\/10.1038\/299802a0 10.1038\/299802a0","DOI":"10.1038\/299802a0"},{"key":"e_1_2_1_61_1","doi-asserted-by":"crossref","unstructured":"N. S. Yanofsky and M. Mannucci. 2008. Quantum Computing for Computer Scientists. Cambridge University Press. isbn:978-0-521-87996-5","DOI":"10.1017\/CBO9780511813887"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","unstructured":"M. Ying. 2016. Foundations of quantum programming. Morgan Kaufmann. isbn:0128023066 https:\/\/doi.org\/10.1016\/C2014-0-02660-3 10.1016\/C2014-0-02660-3","DOI":"10.1016\/C2014-0-02660-3"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","unstructured":"M. Ying and Z. Zhang. 2023. Quantum recursive programming with quantum case statements. (2023). https:\/\/doi.org\/10.48550\/arXiv.2311.01725 arXiv:2311.01725. 10.48550\/arXiv.2311.01725","DOI":"10.48550\/arXiv.2311.01725"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729283"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776731","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:01:09Z","timestamp":1767898869000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776731"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":64,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776731"],"URL":"https:\/\/doi.org\/10.1145\/3776731","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}