{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:22:25Z","timestamp":1765617745132,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","funder":[{"name":"European Union - NextGenerationEU through the Italian Ministry of University and Research","award":["CN00000013 \u201cNational Centre for HPC, Big Data and Quantum Computing\u201d"],"award-info":[{"award-number":["CN00000013 \u201cNational Centre for HPC, Big Data and Quantum Computing\u201d"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,10]]},"DOI":"10.1145\/3756907.3756908","type":"proceedings-article","created":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:11Z","timestamp":1765617551000},"page":"1-3","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Counting Qubits and Gates: Resource Analysis in Quantum Programming Languages"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Bologna, Bologna, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,12,13]]},"reference":[{"key":"e_1_3_3_1_2_2","unstructured":"2025. Quantum error correction below the surface code threshold. Nature 638 8052 (2025) 920\u2013926."},{"key":"e_1_3_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_2"},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533332"},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Kevin Batz Benjamin\u00a0Lucien Kaminski Joost-Pieter Katoen and Christoph Matheja. 2021. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5 POPL (2021) 1\u201330.","DOI":"10.1145\/3434320"},{"key":"e_1_3_3_1_6_2","doi-asserted-by":"crossref","unstructured":"Stephen Bellantoni and Stephen Cook. 1992. A New Recursion-Theoretic Characterization of the Polytime Functions. Computational Complexity 2 (1992) 97\u2013110.","DOI":"10.1007\/BF01201998"},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"crossref","unstructured":"Dolev Bluvstein Simon\u00a0J Evered Alexandra\u00a0A Geim Sophie\u00a0H Li Hengyun Zhou Tom Manovitz Sepehr Ebadi Madelyn Cain Marcin Kalinowski Dominik Hangleiter et\u00a0al. 2024. Logical quantum processor based on reconfigurable atom arrays. Nature 626 7997 (2024) 58\u201365.","DOI":"10.1038\/s41586-023-06927-3"},{"key":"e_1_3_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_1"},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"crossref","unstructured":"Andrea Colledan and Ugo\u00a0Dal Lago. 2025. Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages. Proc. ACM Program. Lang. 9 POPL (2025) 1386\u20131416.","DOI":"10.1145\/3704883"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Andrew Cross Ali Javadi-Abhari Thomas Alexander Niel De\u00a0Beaudrap Lev\u00a0S. Bishop Steven Heidel Colm\u00a0A. Ryan Prasahnt Sivarajah John Smolin Jay\u00a0M. Gambetta and Blake\u00a0R. Johnson. 2022. OpenQASM 3: A Broader and Deeper Quantum Assembly Language. ACM Transactions on Quantum Computing 3 3 (Sept. 2022) 1\u201350. 10.1145\/3505636","DOI":"10.1145\/3505636"},{"key":"e_1_3_3_1_11_2","unstructured":"Andrew\u00a0W. Cross Lev\u00a0S. Bishop John\u00a0A. Smolin and Jay\u00a0M. Gambetta. 2017. Open Quantum Assembly Language. arxiv:https:\/\/arXiv.org\/abs\/1707.03429\u00a0[quant-ph] https:\/\/arxiv.org\/abs\/1707.03429"},{"key":"e_1_3_3_1_12_2","doi-asserted-by":"publisher","unstructured":"Ugo Dal\u00a0Lago Andrea Masini and Margherita Zorzi. 2009. On a measurement-free quantum lambda calculus with classical control. Math. Struct. Comput. Sci. 19 2 (2009) 297\u2013335. 10.1017\/S096012950800741X","DOI":"10.1017\/S096012950800741X"},{"key":"e_1_3_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Ugo Dal\u00a0Lago Andrea Masini and Margherita Zorzi. 2010. Quantum implicit computational complexity. Theor. Comput. Sci. 411 2 (2010) 377\u2013409. 10.1016\/J.TCS.2009.07.045","DOI":"10.1016\/J.TCS.2009.07.045"},{"key":"e_1_3_3_1_14_2","doi-asserted-by":"crossref","unstructured":"Edsger\u00a0W Dijkstra. 1975. Guarded commands nondeterminacy and formal derivation of programs. Commun. ACM 18 8 (1975) 453\u2013457.","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"crossref","unstructured":"Yuan Feng and Mingsheng Ying. 2021. Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing 2 4 (2021) 1\u201343.","DOI":"10.1145\/3456877"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. 1998. Light Linear Logic. Information and Computation 143(2) (1998) 175\u2013204.","DOI":"10.1006\/inco.1998.2700"},{"key":"e_1_3_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38986-3_10"},{"key":"e_1_3_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Alexander\u00a0S. Green Peter\u00a0LeFanu Lumsdaine Neil\u00a0J. Ross Peter Selinger and Beno\u00eet Valiron. 2013. Quipper: a scalable quantum programming language. ACM SIGPLAN Notices 48 6 (June 2013) 333\u2013342. 10.1145\/2499370.2462177","DOI":"10.1145\/2499370.2462177"},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30829-1_8"},{"key":"e_1_3_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Ali Javadi-Abhari Matthew Treinish Kevin Krsulich Christopher\u00a0J. Wood Jake Lishman Julien Gacon Simon Martiel Paul\u00a0D. Nation Lev\u00a0S. Bishop Andrew\u00a0W. Cross Blake\u00a0R. Johnson and Jay\u00a0M. Gambetta. 2024. Quantum computing with Qiskit. 10.48550\/arXiv.2405.08810 arxiv:https:\/\/arXiv.org\/abs\/2405.08810\u00a0[quant-ph]","DOI":"10.48550\/arXiv.2405.08810"},{"key":"e_1_3_3_1_22_2","doi-asserted-by":"publisher","unstructured":"M.\u00a0W. Johnson M.\u00a0H.\u00a0S. Amin S. Gildert T. Lanting F. Hamze N. Dickson R. Harris A.\u00a0J. Berkley J. Johansson P. Bunyk E.\u00a0M. Chapple C. Enderud J.\u00a0P. Hilton K. Karimi E. Ladizinsky N. Ladizinsky T. Oh I. Perminov C. Rich M.\u00a0C. Thom E. Tolkacheva C.\u00a0J.\u00a0S. Truncik S. Uchaikin J. Wang B. Wilson and G. Rose. 2011. Quantum annealing with manufactured spins. Nature 473 7346 (2011) 194\u2013198. 10.1038\/nature10012","DOI":"10.1038\/nature10012"},{"key":"e_1_3_3_1_23_2","doi-asserted-by":"publisher","unstructured":"A.Yu. Kitaev. 2003. Fault-tolerant quantum computation by anyons. Annals of Physics 303 1 (2003) 2\u201330. 10.1016\/S0003-4916(02)00018-0","DOI":"10.1016\/S0003-4916(02)00018-0"},{"key":"e_1_3_3_1_24_2","doi-asserted-by":"publisher","unstructured":"E Knill. 1996. Conventions for quantum pseudocode. Technical report (6 1996). 10.2172\/366453","DOI":"10.2172\/366453"},{"key":"e_1_3_3_1_25_2","doi-asserted-by":"crossref","unstructured":"Yves Lafont. 2004. Soft linear logic and polynomial time. Theor. Comput. Sci. 318 1-2 (2004) 163\u2013180.","DOI":"10.1016\/S0304-3975(03)00523-1"},{"key":"e_1_3_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158659"},{"key":"e_1_3_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139034807"},{"key":"e_1_3_3_1_28_2","doi-asserted-by":"crossref","unstructured":"Junyi Liu Li Zhou Gilles Barthe and Mingsheng Ying. 2025. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. J. ACM 72 3 (2025) 20:1\u201320:51.","DOI":"10.1145\/3734516"},{"key":"e_1_3_3_1_29_2","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"McIver Annabelle","year":"2005","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer."},{"key":"e_1_3_3_1_30_2","doi-asserted-by":"crossref","unstructured":"John Preskill. 2018. Quantum computing in the NISQ era and beyond. Quantum 2 (2018) 79.","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_3_3_1_31_2","doi-asserted-by":"crossref","unstructured":"Peter Selinger and Beno\u00eet Valiron. 2006. A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci. 16 3 (2006) 527\u2013552.","DOI":"10.1017\/S0960129506005238"},{"key":"e_1_3_3_1_32_2","doi-asserted-by":"crossref","unstructured":"Peter Selinger and Beno\u00eet Valiron. 2008. On a fully abstract model for a quantum linear functional language. Electronic Notes in Theoretical Computer Science 210 (2008) 123\u2013137.","DOI":"10.1016\/j.entcs.2008.04.022"},{"key":"e_1_3_3_1_33_2","doi-asserted-by":"crossref","unstructured":"Peter\u00a0W Shor. 1999. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM review 41 2 (1999) 303\u2013332.","DOI":"10.1137\/S0036144598347011"},{"key":"e_1_3_3_1_34_2","unstructured":"Google AI\u00a0Quantum Team. 2018. Cirq Programming Language. https:\/\/quantumai.google\/cirq."},{"key":"e_1_3_3_1_35_2","doi-asserted-by":"crossref","unstructured":"Tomoyuki Yamakami. 2020. A Schematic Definition of quantum Polynomial Time Computability. J. Symb. Log. 85 4 (2020) 1546\u20131587.","DOI":"10.1017\/jsl.2020.45"},{"key":"e_1_3_3_1_36_2","doi-asserted-by":"crossref","unstructured":"Tomoyuki Yamakami. 2024. Elementary quantum recursion schemes that capture quantum polylogarithmic-time computability of quantum functions. Math. Struct. Comput. Sci. 34 7 (2024) 710\u2013745.","DOI":"10.1017\/S0960129524000264"}],"event":{"name":"PPDP '25: Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming","location":"Rende Italy","acronym":"PPDP '25"},"container-title":["Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3756907.3756908","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:57Z","timestamp":1765617597000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3756907.3756908"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,10]]},"references-count":35,"alternative-id":["10.1145\/3756907.3756908","10.1145\/3756907"],"URL":"https:\/\/doi.org\/10.1145\/3756907.3756908","relation":{},"subject":[],"published":{"date-parts":[[2025,9,10]]},"assertion":[{"value":"2025-12-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}