{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T01:47:39Z","timestamp":1787017659157,"version":"build-2736575974"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100021856","name":"Ministero dell'Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","award":["CN00000013"],"award-info":[{"award-number":["CN00000013"]}],"id":[{"id":"10.13039\/501100021856","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    We introduce a type system for the\n                    <jats:monospace>Quipper<\/jats:monospace>\n                    language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including\n                    <jats:italic toggle=\"yes\">width<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">depth<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">gate count<\/jats:italic>\n                    , but also variations thereof obtained by considering only\n                    <jats:italic toggle=\"yes\">some<\/jats:italic>\n                    wire types or\n                    <jats:italic toggle=\"yes\">some<\/jats:italic>\n                    gate kinds. The key ingredients for achieving this level of flexibility are effects and refinement types, both relying on\n                    <jats:italic toggle=\"yes\">indices<\/jats:italic>\n                    , that is, generic arithmetic expressions whose operators are interpreted differently depending on the target metric. The approach is shown to be correct through logical predicates, under reasonable assumptions about the chosen resource metric. This approach is empirically evaluated through the\n                    <jats:monospace>QuRA<\/jats:monospace>\n                    tool, showing that, in many cases, inferring tight bounds is possible in a fully automatic way.\n                  <\/jats:p>","DOI":"10.1145\/3704883","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1386-1416","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0049-0391","authenticated-orcid":false,"given":"Andrea","family":"Colledan","sequence":"first","affiliation":[{"name":"University of Bologna, Bologna, Italy"},{"name":"Inria, Valbonne, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Bologna, Italy"},{"name":"Inria, Valbonne, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Elvira Albert Puri Arenas Samir Genaim German Puebla and Damiano Zanardini. 2008. COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In Proc. ofFMCO 2007. 113-132. https:\/\/doi.org\/10.1007\/978-3-540-92188-2_5 10.1007\/978-3-540-92188-2_5.","DOI":"10.1007\/978-3-540-92188-2_5"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Matthew Amy Olivia Di Matteo Vlad Gheorghiu Michele Mosca Alex Parent and John Schanck. 2017. Estimating the Cost of Generic Quantum Pre-image Attacks on SHA-2 and SHA-3. In Proc. of SAC 2016. 317-337. https:\/\/doi.org\/10.1007\/978-3-319-69453-5_18 10.1007\/978-3-319-69453-5_18","DOI":"10.1007\/978-3-319-69453-5_18"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Martin Avanzini Ugo Dal Lago and Alexis Ghyselen. 2019. Type-Based Complexity Analysis of Probabilistic Functional Programs. In Proc. of LICS 2019 1-13. https:\/\/doi.org\/10.1109\/LICS.2019.8785725 10.1109\/LICS.2019.8785725","DOI":"10.1109\/LICS.2019.8785725"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Martin Avanzini Georg Moser Romain Pechoux Simon Perdrix and Vladimir Zamdzhiev. 2022. Quantum Expectation Transformers for Cost Analysis. In Proc. of LICS 2022 1-13. https:\/\/doi.org\/10.1145\/3531130.3533332 10.1145\/3531130.3533332","DOI":"10.1145\/3531130.3533332"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Raphaelle Crubille Ugo Dal Lago and Francesco Gavazzo. 2020. On the Versatility of Open Logical Relations. In Proc. of ESOP 2020 56-83. https:\/\/doi.org\/10.1007\/978-3-030-44914-8_3 10.1007\/978-3-030-44914-8_3","DOI":"10.1007\/978-3-030-44914-8_3"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA336"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2022.3"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Andrea Colledan and Ugo Dal Lago. 2024. Circuit Width Estimation via Effect Typing and Linear Dependency. In Proc. of ESOP 2024 3-30. https:\/\/doi.org\/10.1007\/978-3-031-57267-8_1 10.1007\/978-3-031-57267-8_1","DOI":"10.1007\/978-3-031-57267-8_1"},{"key":"e_1_3_2_10_2","unstructured":"Hugh Collins and Chris Nay. 2022. IBM Unveils 400 Qubit-Plus Quantum Processor and Next-Generation IBM Quantum System Two. https:\/\/is.gd\/WPV7lO Retrieved on Nov. 10 2024."},{"key":"e_1_3_2_11_2","unstructured":"Emily Conover. 2020. Light-based Quantum Computer Jiuzhang achieves quantum supremacy.https:\/\/is.gd\/zIgFzK retrieved on Nov. 10 2024."},{"key":"e_1_3_2_12_2","unstructured":"D. Coppersmith. 2002. An approximate Fourier transform useful in quantum factoring IBM Research Report RC19642. arXiv:quant-ph\/0201067"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3505636"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Proc. of LICS 2011. 133-142. https:\/\/doi.org\/10.1109\/LICS.2011.22 10.1109\/LICS.2011.22","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2022.37"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.045"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Barbara Petit. 2012. Linear Dependent Types in a Call-by-Value Scenario. In Proc. ofPPDP 2012 115-126. https:\/\/doi.org\/10.1145\/2370776.2370792 10.1145\/2370776.2370792","DOI":"10.1145\/2370776.2370792"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Barbara Petit. 2013. The Geometry ofTypes. In Proc. ofPOPL 2013 167-178. https:\/\/doi.org\/10.1145\/2429069.2429090 10.1145\/2429069.2429090","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236786"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.13"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Ankush Das Di Wang and Jan Hoffmann. 2023. Probabilistic Resource-Aware Session Types. In Proc. of POPL 2023. 32 pages. https:\/\/doi.org\/10.1145\/3571259 10.1145\/3571259","DOI":"10.1145\/3571259"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Cirq Developers. 2024. Cirq. https:\/\/doi.org\/10.5281\/zenodo.11398048 10.5281\/zenodo.11398048","DOI":"10.5281\/zenodo.11398048"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Tim Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proc. of PLDI 1991. 268-277. https:\/\/doi.org\/10.1145\/113445.113468 10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Peng Fu Kohei Kishida Neil J. Ross and Peter Selinger. 2023. Proto-Quipper with Dynamic Lifting. In Proc. of POPL 2023 309-334. https:\/\/doi.org\/10.1145\/3571204 10.1145\/3571204","DOI":"10.1145\/3571204"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Peng Fu Kohei Kishida and Peter Selinger. 2020. Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. In Proc. of LICS 2020 440-453. https:\/\/doi.org\/10.1145\/3373718.3394765 10.1145\/3373718.3394765","DOI":"10.1145\/3373718.3394765"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Marco Gaboardi Andreas Haeberlen Justin Hsu Arjun Narayan and Benjamin C. Pierce. 2013. Linear Dependent Types for Differential Privacy. In Proc. of POPL 2013 357-370. https:\/\/doi.org\/10.1145\/2429069.2429113 10.1145\/2429069.2429113","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_3_2_29_2","unstructured":"Sukhpal Singh Gill Oktay Cetinkaya Stefano Marrone Daniel Claudino David Haunschild Leon Schlote Huaming Wu Carlo Ottaviani Xiaoyuan Liu Sree Pragna Machupalli Kamalpreet Kaur Priyansh Arora Ji Liu Ahmed Farouk Houbing Herbert Song Steve Uhlig and Kotagiri Ramamohanarao. 2024. Quantum Computing: Vision and Challenges. arXiv:2403.02240"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Markus Grassl Brandon Langenberg Martin Roetteler and Rainer Steinwandt. 2016. Applying Grover\u2019s Algorithm to AES: Quantum Resource Estimates. In Proc. ofPQCrypto 2016. 29-43. https:\/\/doi.org\/10.1007\/978-3-319-29360-8_3 10.1007\/978-3-319-29360-8_3","DOI":"10.1007\/978-3-319-29360-8_3"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Alexander S. Green Peter LeFanu Lumsdaine Neil J. Ross Peter Selinger and Beno\u00cet Valiron. 2013. Quipper. In Proc. of PLDI 333-342. https:\/\/doi.org\/10.1145\/2499370.2462177 10.1145\/2499370.2462177","DOI":"10.1145\/2499370.2462177"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Alexander S. Green Peter LeFanu Lumsdaine Neil J. Ross Peter Selinger and Beno\u00cet Valiron. 2013. Quipper: a scalable quantum programming language. In Proc. ofPLDI 2013 333-342. https:\/\/doi.org\/10.1145\/2491956.2462177 10.1145\/2491956.2462177","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","unstructured":"LovK. Grover. 1996. A fast quantum mechanical algorithm for database search. arXiv:arXiv:quant-ph\/9605043","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_7"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Thomas H\u00e0ner Torsten Hoefler and Matthias Troyer. 2020. Assertion-based optimization of Quantum programs. In Proc. of OOPSLA 2020 1-20. https:\/\/doi.org\/10.1145\/3428201 10.1145\/3428201","DOI":"10.1145\/3428201"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2021.21"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Kesha Hietala Robert Rand Shih-Han Hung Xiaodi Wu and Michael Hicks. 2021. A verified optimizer for Quantum circuits. In Proc. ofPOPL 2021 1-29. https:\/\/doi.org\/10.1145\/3434318 10.1145\/3434318","DOI":"10.1145\/3434318"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000487"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"John Hughes Lars Pareto and Amr Sabry. 1996. Proving the correctness of reactive systems using sized types. In Proc. ofPOPL 1996 410-423. https:\/\/doi.org\/10.1145\/237721.240882 10.1145\/237721.240882","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Shih-Han Hung Kesha Hietala Shaopeng Zhu Mingsheng Ying Michael Hicks and Xiaodi Wu. 2019. Quantitative robustness analysis of quantum programs. In Proc. ofPOPL 2019. 31:1-31:29. https:\/\/doi.org\/10.1145\/3290344 10.1145\/3290344","DOI":"10.1145\/3290344"},{"key":"e_1_3_2_42_2","unstructured":"Ali Javadi-Abhari Matthew Treinish Kevin Krsulich Christopher J. Wood Jake Lishman Julien Gacon Simon Martiel Paul D. Nation Lev S. Bishop Andrew W. Cross Blake R. Johnson and Jay M. Gambetta. 2024. Quantum computing with Qiskit. arXiv:2405.08810"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656428"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In Proc. of ESOP 2016 364-389. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15 10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_45_2","unstructured":"E. Knill. 2022. Conventions for Quantum Pseudocode. arXiv:2211.02559"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293605"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2021.51"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3624483"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Yangjia Li and Mingsheng Ying. 2018. Algorithmic analysis of termination problems for quantum programs. In Proc. of POPL 2018. 35:1-35:29. https:\/\/doi.org\/10.1145\/3158123 10.1145\/3158123","DOI":"10.1145\/3158123"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-013-0185-3"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Junyi Liu Li Zhou Gilles Barthe and Mingsheng Ying. 2022. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. In Proc. ofLICS 2022 1-13. https:\/\/doi.org\/10.1145\/3531130.3533327 10.1145\/3531130.3533327","DOI":"10.1145\/3531130.3533327"},{"key":"e_1_3_2_52_2","unstructured":"John Martinis. 2019. Quantum supremacy using a programmable superconducting processor. https:\/\/is.gd\/v3VXFi Retrieved on Nov. 10 2024."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Alan Mycroft Dominic Orchard and Tomas Petricek. 2016. Effect Systems Revisited\u2014Control-Flow Algebra and Semantics. In Semantics Logics and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion ofTheir 60th Birthdays 1-32. https:\/\/doi.org\/10.1007\/978-3-319-27810-0 10.1007\/978-3-319-27810-0","DOI":"10.1007\/978-3-319-27810-0"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Tomas Petricek Dominic Orchard and Alan Mycroft. 2014. Coeffects: A calculus of context-dependent computation. In Proc. ofICFP2014 123-135. https:\/\/doi.org\/10.1145\/2628136.2628160 10.1145\/2628136.2628160","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/1568318.1568324"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.11"},{"key":"e_1_3_2_59_2","volume-title":"Algebraic and Logical Methods in Quantum Computation","author":"Ross Neil","year":"2015","unstructured":"Neil Ross. 2015. Algebraic and Logical Methods in Quantum Computation. Ph. D. Dissertation. Dalhousie University."},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_47"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","unstructured":"Maximilian Schlosshauer. 2007. Decoherence and the Quantum-To-Classical Transition. Springer Berlin Heidelberg. https:\/\/doi.org\/10.1007\/978-3-540-35775-9 10.1007\/978-3-540-35775-9","DOI":"10.1007\/978-3-540-35775-9"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"Peter Selinger. 2004. A Brief Survey of Quantum Programming Languages. In Proc. of FLOPS 2004. 1-6. https:\/\/doi.org\/10.1007\/978-3-540-24754-8_1 10.1007\/978-3-540-24754-8_1","DOI":"10.1007\/978-3-540-24754-8_1"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","unstructured":"P.W. Shor. 1994. Algorithms for quantum computation: discrete logarithms and factoring. In Proc. of FOCS 1994. 124-134. https:\/\/doi.org\/10.1109\/sfcs.1994.365700 10.1109\/sfcs.1994.365700","DOI":"10.1109\/sfcs.1994.365700"},{"key":"e_1_3_2_64_2","unstructured":"Lau Skorstengaard. 2019. An Introduction to Logical Relations. arXiv:1907.11133"},{"key":"e_1_3_2_65_2","unstructured":"Aarthi Sundaram Robert Rand Kartik Singhal and Brad Lackey. 2022. A Rich Type System for Quantum Programs. arXiv:2101.08939"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"Niki Vazou Eric L. Seidel Ranjit Jhala Dimitrios Vytiniotis and Simon Peyton-Jones. 2014. Refinement types for Haskell. In Proc. of ICFP 2014 269-282. https:\/\/doi.org\/10.1145\/2628136.2628161 10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JCSS.2020.08.004"},{"key":"e_1_3_2_68_2","volume-title":"Quantum machine learning: what quantum computing means to data mining","author":"Wittek Peter","year":"2014","unstructured":"Peter Wittek. 2014. Quantum machine learning: what quantum computing means to data mining. Academic Press."},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2020.45"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704883","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704883","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:21Z","timestamp":1770200061000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704883"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":68,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704883"],"URL":"https:\/\/doi.org\/10.1145\/3704883","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}