{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:56:13Z","timestamp":1758056173327,"version":"3.44.0"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"name":"European Union\u2014NextGenerationEU through the Italian Ministry of University and Research","award":["CN00000013"],"award-info":[{"award-number":["CN00000013"]}]},{"name":"ERC starting Grant CRETE","award":["101039196"],"award-info":[{"award-number":["101039196"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n            Circuit description languages are a class of quantum programming languages in which programs are classical and produce a\n            <jats:italic toggle=\"yes\">description<\/jats:italic>\n            of a quantum computation, in the form of a\n            <jats:italic toggle=\"yes\">quantum circuit<\/jats:italic>\n            . Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this article, we present\n            <jats:sans-serif>Proto-Quipper-R<\/jats:sans-serif>\n            , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. Lastly, we introduce\n            <jats:monospace>QuRA<\/jats:monospace>\n            , a static analysis tool based on\n            <jats:sans-serif>Proto-Quipper-R<\/jats:sans-serif>\n            \u2019s type system, and use it to show that our framework allows for the automatic width verification of realistic quantum algorithms, such as the QFT and Grover\u2019s algorithm.\n          <\/jats:p>","DOI":"10.1145\/3737282","type":"journal-article","created":{"date-parts":[[2025,5,23]],"date-time":"2025-05-23T21:57:38Z","timestamp":1748037458000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Circuit Width Estimation via Effect Typing and Linear\u00a0Dependency"],"prefix":"10.1145","volume":"47","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 and INRIA Sophia Antipolis, Sophia Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo Dal","family":"Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Bologna, Italy and INRIA Sophia Antipolis, Sophia Antipolis, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0732-5476","authenticated-orcid":false,"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software, Pozuelo de Alarc\u00f3n, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_3_2_3_2","article-title":"Efficient quantum modular arithmetics for the ISQ era","author":"Atchade-Adelomou Parfait","year":"2023","unstructured":"Parfait Atchade-Adelomou and Saul Gonzalez. 2023. Efficient quantum modular arithmetics for the ISQ era. arXiv:2311.08555. Retrieved from https:\/\/arxiv.org\/abs\/2311.08555","journal-title":"arXiv:2311.08555"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_3_2_5_2","first-page":"130","volume-title":"Proc. of FLOPS 2008","author":"Avanzini Martin","year":"2008","unstructured":"Martin Avanzini and Georg Moser. 2008. Complexity analysis by rewriting. In Proc. of FLOPS 2008. Springer, Berlin, 130\u2013146."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2013.71"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533332"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_9_2","volume-title":"The SMT-LIB Standard: Version 2.6","author":"Barrett Clark","year":"2017","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Retrieved from www.SMT-LIB.org"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129740"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA336"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2022.3"},{"key":"e_1_3_2_13_2","unstructured":"Hugh Collins and Chris Nay. 2022. IBM Unveils 400 Qubit-Plus Quantum Processor and Next-Generation IBM Quantum System Two. Retrieved June 6 2025 from https:\/\/is.gd\/WPV7lO"},{"key":"e_1_3_2_14_2","unstructured":"Emily Conover. 2020. Light-Based Quantum Computer Jiuzhang Achieves Quantum Supremacy. Retrieved June 6 2025 from https:\/\/is.gd\/zIgFzK"},{"key":"e_1_3_2_15_2","unstructured":"D. Coppersmith. 2002. An approximate Fourier transform useful in quantum factoring IBM research report RC19642. arXiv:quant-ph\/0201067. Retrieved from https:\/\/arxiv.org\/abs\/quant-ph\/0201067"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3505636"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.045"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2370776.2370792"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_3_2_21_2","unstructured":"Richard Eisenberg Alexander Green Peter Lumsdaine Keith Kim Siun-Chuon Mau Baranidharan Mohan Won Ng Joel Ravelomanantsoa-Ratsimihah Neil Ross Artur Scherer et al. 2019. Quipper.Libraries.QFT. Retrieved June 6 2025 from https:\/\/is.gd\/AEJmp9"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pone.0208561"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proc. of PLDI 1991. ACM 268\u2013277. DOI: 10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","unstructured":"Florian Frohn and J\u00fcrgen Giesl. 2017. Complexity analysis for Java with AProVE. In Proc. of IFM 2017. Springer International Publishing 85\u2013101.","DOI":"10.1007\/978-3-319-66845-1_6"},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","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 Proc. of RC. Springer International Publishing 153\u2013168.","DOI":"10.1007\/978-3-030-52482-1_9"},{"key":"e_1_3_2_26_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. ACM. DOI: 10.1145\/3571204","DOI":"10.1145\/3571204"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394765"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19580-8"},{"key":"e_1_3_2_31_2","first-page":"110","volume-title":"Proc. of RC","author":"Green Alexander S.","year":"2013","unstructured":"Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Beno\u00eet Valiron. 2013. An introduction to quantum programming in Quipper. In Proc. of RC. Springer, Berlin, 110\u2013124."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462177"},{"key":"e_1_3_2_33_2","unstructured":"Lov K. Grover. 1996. A fast quantum mechanical algorithm for database search. arXiv:quant-ph\/9605043. Retrieved from https:\/\/arxiv.org\/abs\/quant-ph\/9605043"},{"key":"e_1_3_2_34_2","unstructured":"Emmanuel Hainry and Romain P\u00e9choux. 2013. Type-Based Heap and Stack Space Analysis in Java. Technical Report."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30829-1"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","first-page":"781","DOI":"10.1007\/978-3-642-31424-7_64","volume-title":"Computer Aided Verification.","author":"Hoffmann Jan","year":"2012","unstructured":"Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Resource aware ML. In Computer Aided Verification. P. Madhusudan and Sanjit A. Seshia (Eds.), Springer, Berlin, 781\u2013786."},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/978-3-642-11957-6_16","volume-title":"Programming Languages and Systems","author":"Hoffmann Jan","year":"2010","unstructured":"Jan Hoffmann and Martin Hofmann. 2010. Amortized resource analysis with polynomial potential. In Programming Languages and Systems. Andrew D. Gordon (Ed.), Springer, Berlin, 287\u2013306."},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Ranjit Jhala and Niki Vazou. 2020. Refinement types: A tutorial. arXiv:2010.07763. Retrieved from https:\/\/arxiv.org\/abs\/2010.07763","DOI":"10.1561\/9781680838855"},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/978-3-662-49498-1_15","volume-title":"Programming Languages and Systems","author":"Kaminski Benjamin Lucien","year":"2016","unstructured":"Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest precondition reasoning for expected run-times of probabilistic programs. In Programming Languages and Systems. Peter Thiemann (Ed.), Springer, Berlin, 364\u2013389."},{"key":"e_1_3_2_42_2","unstructured":"E. Knill. 2022. Conventions for quantum pseudocode. arXiv:2211.02559. Retrieved from https:\/\/arxiv.org\/abs\/2211.02559"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2021.51"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533327"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944725"},{"key":"e_1_3_2_46_2","unstructured":"John Martinis. 2019. Quantum Supremacy Using a Programmable Superconducting Processor. Retrieved June 6 2025 from https:\/\/is.gd\/v3VXFi"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9277-6"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3355759"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_52_2","unstructured":"John Preskill. 2012. Quantum computing and the entanglement frontier. arXiv:1203.5813. Retrieved from https:\/\/arxiv.org\/abs\/1203.5813"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.11"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_55_2","unstructured":"Neil Ross. 2015. Algebraic and Logical Methods in Quantum Computation. Ph.D. Dissertation. Dalhousie University."},{"key":"e_1_3_2_56_2","first-page":"80","volume-title":"Proc. of MPC 2000","author":"Sanders J. W.","year":"2000","unstructured":"J. W. Sanders and P. Zuliani. 2000. Quantum programming. In Proc. of MPC 2000. Springer, Berlin, 80\u201399."},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-35775-9"},{"key":"e_1_3_2_58_2","first-page":"1","volume-title":"Proc. of FLOPS 2004","author":"Selinger Peter","year":"2004","unstructured":"Peter Selinger. 2004. A brief survey of quantum programming languages. In Proc. of FLOPS 2004, 1\u20136."},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/11417170"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1109\/sfcs.1994.365700"},{"key":"e_1_3_2_62_2","article-title":"An introduction to logical relations","author":"Skorstengaard Lau","year":"2019","unstructured":"Lau Skorstengaard. 2019. An introduction to logical relations. arXiv:1907.11133. Retrieved from https:\/\/arxiv.org\/ abs\/1907.11133","journal-title":"arXiv:1907.11133"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-017-0319-z"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","unstructured":"Benoit Valiron. 2016. Automated Parametric Gate Count of Quantum Programs. DOI: 10.14288\/1.0319340","DOI":"10.14288\/1.0319340"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.54.147"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2020.45"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.5555\/1408782"},{"key":"e_1_3_2_70_2","volume-title":"Foundations of Quantum Programming","author":"Mingsheng Ying","year":"2016","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming (1st ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA.","edition":"1"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10773-005-7071-x"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3737282","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T13:53:06Z","timestamp":1757944386000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3737282"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"references-count":71,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3737282"],"URL":"https:\/\/doi.org\/10.1145\/3737282","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"2024-04-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-05-13","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}