{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:12:26Z","timestamp":1784211146920,"version":"3.55.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/X025551\/1"],"award-info":[{"award-number":["EP\/X025551\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Sapere Aude: DFF-Research Leader","award":["5251-00024B"],"award-info":[{"award-number":["5251-00024B"]}]}],"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>\n                    Quantum computing offers advantages over classical computation, yet the precise features that set the two apart remain unclear. In the standard quantum circuit model, adding a 1-qubit basis-changing gate\u2014commonly chosen to be the Hadamard gate\u2014to a universal set of classical reversible gates yields computationally universal quantum computation. However, the computational behaviours enabled by this addition are not fully characterised. We give such a characterisation by introducing a small quantum programming language extending the universal classical reversible programming language \u03a0 with a single primitive corresponding to the Hadamard gate. The language comes equipped with a sound and complete categorical semantics that is specified by a purely equational theory. Completeness is shown by means of a novel finite presentation, and a corresponding synthesis algorithm, for the groups of orthogonal matrices with entries in the ring\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mi>z<\/mml:mi>\n                          <mml:mo stretchy=\"false\">[<\/mml:mo>\n                          <mml:mfrac>\n                            <mml:mn>1<\/mml:mn>\n                            <mml:mrow>\n                              <mml:msqrt>\n                                <mml:mn>2<\/mml:mn>\n                              <\/mml:msqrt>\n                            <\/mml:mrow>\n                          <\/mml:mfrac>\n                          <mml:mo stretchy=\"false\">]<\/mml:mo>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3776647","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"117-143","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Hadamard-Pi: Equational Quantum Programming"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7628-1185","authenticated-orcid":false,"given":"Wang","family":"Fang","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7393-2640","authenticated-orcid":false,"given":"Chris","family":"Heunen","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7672-799X","authenticated-orcid":false,"given":"Robin","family":"Kaarsgaard","sequence":"additional","affiliation":[{"name":"University of Southern Denmark, Odense, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"D. Aharonov. 2003. A Simple Proof that Toffoli and Hadamard are Quantum Universal. arXiv:quant-ph\/0301040 [quant-ph] https:\/\/arxiv.org\/abs\/quant-ph\/0301040"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38100-3_12"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2020-04-06-252"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"M. Backens and A. Kissinger. 2018. ZH: A complete graphical calculus for quantum computations involving classical non-linearity. In Quantum Physics and Logic (Electronic Proceedings in Theoretical Computer Science Vol. 287). 23\u201342. https:\/\/doi.org\/10.4204\/EPTCS.287.2 10.4204\/EPTCS.287.2","DOI":"10.4204\/EPTCS.287.2"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"X. Bian and P. Selinger. 2021. Generators and relations for Un(\u2124[12 i]). In Quantum Physics and Logic (Electronic Proceedings in Theoretical Computer Science Vol. 343). 145\u2013164. https:\/\/doi.org\/10.4204\/EPTCS.343.8 10.4204\/EPTCS.343.8","DOI":"10.4204\/EPTCS.343.8"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.394.2"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674625"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632861"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/bs.adcom.2021.11.009"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"J. Carette and A. Sabry. 2016. Computing with Semirings and Weak Rig Groupoids. In Programming Languages and Systems (ESOP 2016). 123\u2013148. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_6 10.1007\/978-3-662-49498-1_6","DOI":"10.1007\/978-3-662-49498-1_6"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498667"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"A. Cl\u00e9ment N. Delorme and S. Perdrix. 2024a. Minimal Equational Theories for Quantum Circuits. In Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201924). Article 27 14 pages. https:\/\/doi.org\/10.1145\/3661814.3662088 10.1145\/3661814.3662088","DOI":"10.1145\/3661814.3662088"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"A. Cl\u00e9ment N. Delorme S. Perdrix and R. Vilmart. 2024b. Quantum Circuit Completeness: Extensions and Simplifications. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 288). 20:1\u201320:23. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2024.20 10.4230\/LIPIcs.CSL.2024.20","DOI":"10.4230\/LIPIcs.CSL.2024.20"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"A. Cl\u00e9ment N. Heurtel S. Mansfield S. Perdrix and B. Valiron. 2022. LOv calculus: A graphical language for linear optical quantum circuits. In Mathematical Foundations of Computer Science (LIPIcs Vol. 241). 35:1\u201335:16. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2022.35 10.4230\/LIPIcs.MFCS.2022.35","DOI":"10.4230\/LIPIcs.MFCS.2022.35"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"A. Cl\u00e9ment N. Heurtel S. Mansfield S. Perdrix and B. Valiron. 2023. A Complete Equational Theory for Quantum Circuits. In 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201313. https:\/\/doi.org\/10.1109\/LICS56636.2023.10175801 10.1109\/LICS56636.2023.10175801","DOI":"10.1109\/LICS56636.2023.10175801"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"B. Coecke and R. Duncan. 2008. Interacting Quantum Observables. In International Colloquium on Automata Languages and Programming (Lecture Notes in Computer Science Vol. 5126). 298\u2013310. https:\/\/doi.org\/10.1007\/978-3-540-70583-3_25 10.1007\/978-3-540-70583-3_25","DOI":"10.1007\/978-3-540-70583-3_25"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"N. de Beaudrap A. Kissinger and J. van de Wetering. 2022. Circuit extraction for ZX-diagrams can be #P-hard. In International Colloquium on Automata Languages and Programming (ICALP 2022). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2022.119 10.4230\/LIPIcs.ICALP.2022.119","DOI":"10.4230\/LIPIcs.ICALP.2022.119"},{"key":"e_1_3_1_19_1","unstructured":"W. Fang C. Heunen and R. Kaarsgaard. 2025. Hadamard-\u03a0: Equational Quantum Programming (Extended Version). arXiv:2506.06835 [quant-ph] https:\/\/arxiv.org\/abs\/2506.06835"},{"key":"e_1_3_1_20_1","volume-title":"Generators and relations for the group U4(\u2124[1\/2,i])","author":"Greylyn S. E. M.","year":"2014","unstructured":"S. E. M. Greylyn. 2014. Generators and relations for the group U4(\u2124[1\/2,i]). Master\u2019s thesis. Depart ment of Mathematics and Statistics, Dalhousie University. Available at https:\/\/arxiv.org\/abs\/1408.6204."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1038\/s42254-020-00245-7"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498663"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198739623.001.0001"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"R. P. James and A. Sabry. 2012. Information effects. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201912). 73\u201384. https:\/\/doi.org\/10.1145\/2103656.2103667 10.1145\/2103656.2103667","DOI":"10.1145\/2103656.2103667"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"E. Jeandel S. Perdrix and R. Vilmart. 2018. A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics. In Logic in Computer Science. 559\u2013568. https:\/\/doi.org\/10.1145\/3209108.3209131 10.1145\/3209108.3209131","DOI":"10.1145\/3209108.3209131"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/863284"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"M. Laplaza. 1972. Coherence for distributivity. Coherence in Categories (1972) 29\u201365. https:\/\/doi.org\/10.1007\/BFb0059555 10.1007\/BFb0059555","DOI":"10.1007\/BFb0059555"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"S. M. Li N. J. Ross and P. Selinger. 2021. Generators and Relations for the Group On(\u2124[ 1\/2 ]). In Quantum Physics and Logic (Electronic Proceedings in Theoretical Computer Science Vol. 343). 210\u2013264. https:\/\/doi.org\/10.4204\/eptcs.343.11 10.4204\/eptcs.343.11","DOI":"10.4204\/eptcs.343.11"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2011508.2011515"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10701-010-9452-0"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813887"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776647","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:42:02Z","timestamp":1784209322000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776647"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":30,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776647"],"URL":"https:\/\/doi.org\/10.1145\/3776647","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-06-26","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"}}]}}