{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:26Z","timestamp":1767928646688,"version":"3.49.0"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572661","type":"print"},{"value":"9783031572678","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Circuit description languages are a class of quantum programming languages in which programs are classical and produce a <jats:italic>description<\/jats:italic> of a quantum computation, in the form of a <jats:italic>quantum circuit<\/jats:italic>. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present , 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. We also show that our approach is expressive enough to verify realistic quantum algorithms.<\/jats:p>","DOI":"10.1007\/978-3-031-57267-8_1","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:02:01Z","timestamp":1712246521000},"page":"3-30","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Circuit Width Estimation via Effect Typing and Linear Dependency"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0049-0391","authenticated-orcid":false,"given":"Andrea","family":"Colledan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"1_CR1","unstructured":"Altenkirch, T., Grattage, J.: A functional quantum programming language. In: Proc. of LICS \u201905 (2005)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Dal\u00a0Lago, U., Moser, G.: Analysing the complexity of functional programs: Higher-order meets first-order. In: Proc. of ICFP 2015 (2015)","DOI":"10.1145\/2784731.2784753"},{"key":"1_CR3","unstructured":"Avanzini, M., Moser, G.: Complexity analysis by rewriting. In: Proc. of FLOPS 2008 (2008)"},{"key":"1_CR4","unstructured":"Avanzini, M., Moser, G.: Tyrolean Complexity Tool: Features and Usage. In: Proc. of RTA 2013. vol.\u00a021 (2013)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G., Pechoux, R., Perdrix, S., Zamdzhiev, V.: Quantum expectation transformers for cost analysis. In: Proc. of LICS \u201922 (2022)","DOI":"10.1145\/3531130.3533332"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions (extended abstract). In: STOC \u201992 (1992)","DOI":"10.1145\/129712.129740"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336. IOS Press (2021)","DOI":"10.3233\/FAIA336"},{"key":"1_CR8","unstructured":"Colledan, A., Dal\u00a0Lago, U.: On Dynamic Lifting and Effect Typing in Circuit Description Languages. In: TYPES 2022. vol.\u00a0269 (2023)"},{"key":"1_CR9","unstructured":"Collins, H., Nay, C.: Ibm unveils 400 qubit-plus quantum processor and next-generation ibm quantum system two (2022), https:\/\/is.gd\/WPV7lO, retrieved on Oct. 15, 2023"},{"key":"1_CR10","unstructured":"Conover, E.: Light-based quantum computer jiuzhang achieves quantum supremacy (2020), https:\/\/is.gd\/kFv6IOy, retrieved on Oct. 15, 2023"},{"key":"1_CR11","unstructured":"Coppersmith, D.: An approximate fourier transform useful in quantum factoring, ibm research report rc19642 (2002)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Dal\u00a0Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: Proc. of LICS \u201911 (2011)","DOI":"10.1109\/LICS.2011.22"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Dal Lago, U., Masini, A., Zorzi, M.: Quantum implicit computational complexity. TCS 411(2) (2010)","DOI":"10.1016\/j.tcs.2009.07.045"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Dal\u00a0lago, U., Petit, B.: Linear dependent types in a call-by-value scenario. In: Proc. of PPDP \u201912 (2012)","DOI":"10.1145\/2370776.2370792"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Dal\u00a0lago, U., Petit, B.: The geometry of types. In: Proc. of POPL \u201913 (2013)","DOI":"10.1145\/2429069.2429090"},{"key":"1_CR16","unstructured":"Eisenberg, R., Green, A., Lumsdaine, P., Kim, K., Mau, S.C., Mohan, B., Ng, W., Ravelomanantsoa-Ratsimihah, J., Ross, N., Scherer, A., Selinger, P., Valiron, B., Virodov, A., Zdancewic, S.: Quipper.libraries.qft, https:\/\/is.gd\/AEJmp9, retrieved on Oct. 15, 2023"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Fingerhuth, M., Babej, T., Wittek, P.: Open source software in quantum computing. PLOS ONE 13(12) (2018)","DOI":"10.1371\/journal.pone.0208561"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ml. In: Proc. of PLDI \u201991 (1991)","DOI":"10.1145\/113445.113468"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Frohn, F., Giesl, J.: Complexity analysis for java with aprove. In: Proc. of IFM 2017 (2017)","DOI":"10.1007\/978-3-319-66845-1_6"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Fu, P., Kishida, K., Ross, N.J., Selinger, P.: A tutorial introduction to quantum circuit programming in dependently typed proto-quipper. In: Proc. of RC (2020)","DOI":"10.1007\/978-3-030-52482-1_9"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Fu, P., Kishida, K., Ross, N.J., Selinger, P.: Proto-quipper with dynamic lifting. In: Proc. of POPL \u201923 (2023)","DOI":"10.1145\/3571204"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Fu, P., Kishida, K., Selinger, P.: Linear dependent type theory for quantum programming languages: Extended abstract. In: Proc. of LICS \u201920 (2020)","DOI":"10.1145\/3373718.3394765"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: Proc. of POPL \u201913 (2013)","DOI":"10.1145\/2429069.2429113"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Gay, S.J.: Quantum programming languages: Survey and bibliography. Math. Struct. Comput. Sci. 16(4) (2006)","DOI":"10.1017\/S0960129506005378"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: An introduction to quantum programming in quipper. In: Proc. of RC (2013)","DOI":"10.1145\/2491956.2462177"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper. In: Proc. of PLDI (2013)","DOI":"10.1145\/2491956.2462177"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Grover, L.K.: A fast quantum mechanical algorithm for database search (1996)","DOI":"10.1145\/237814.237866"},{"key":"1_CR28","unstructured":"Hainry, E., P\u00e9choux, R.: Type-based heap and stack space analysis in Java (2013), technical report"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Hainry, E., P\u00e9choux, R., Silva, M.: A programming language characterizing quantum polynomial time. In: Proc. of FoSSaCS 2023 (2023)","DOI":"10.1007\/978-3-031-30829-1_8"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Handley, M., Vazou, N., Hutton, G.: Liquidate your assets: reasoning about resource usage in liquid haskell. PACMPL 4 (2019)","DOI":"10.1145\/3371092"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Phys. Rev. Lett. 103 (2009)","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ml. In: Computer Aided Verification (2012)","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Programming Languages and Systems (2010)","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run\u2013times of probabilistic programs. In: Programming Languages and Systems. Berlin, Heidelberg (2016)","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"1_CR35","unstructured":"Lee, D., Perrelle, V., Valiron, B., Xu, Z.: Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In: Proc. of FSTTCS (2021)"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhou, L., Barthe, G., Ying, M.: Quantum weakest preconditions for reasoning about expected runtimes of quantum programs. In: Proc. of LICS \u201922 (2022)","DOI":"10.1145\/3531130.3533327"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proc. of ICFP \u201903 (2003)","DOI":"10.1145\/944705.944725"},{"key":"1_CR38","unstructured":"Martinis, J.: Quantum supremacy using a programmable superconducting processor (2019), https:\/\/is.gd\/v3VXFi, retrieved on Oct. 15, 2023"},{"key":"1_CR39","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R.: Type and effect systems. In: Correct System Design: Recent Insights and Advances. Springer Berlin Heidelberg (1999)","DOI":"10.1007\/3-540-48092-7_6"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. Journal of Automated Reasoning 51(1) (2013)","DOI":"10.1007\/s10817-013-9277-6"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Orchard, D., Liepelt, V.B., Eades\u00a0III, H.: Quantitative program reasoning with graded modal types. In: Proc. of ICFP \u201919. vol.\u00a03 (2019)","DOI":"10.1145\/3342537"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Palsberg, J.: Toward a universal quantum programming language. XRDS: Crossroads 26(1) (2019)","DOI":"10.1145\/3355759"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Paykin, J., Rand, R., Zdancewic, S.: Qwire: A core language for quantum circuits. In: Proc. of POPL \u201917 (2017)","DOI":"10.1145\/3009837.3009894"},{"key":"1_CR45","unstructured":"Preskill, J.: Quantum computing and the entanglement frontier (2012)"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Rios, F., Selinger, P.: A categorical model for a quantum circuit description language. In: Proc. of QPL \u201917. vol.\u00a0266 (2017)","DOI":"10.4204\/EPTCS.266.11"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proc. of PLDI \u201908 (2008)","DOI":"10.1145\/1375581.1375602"},{"key":"1_CR48","unstructured":"Ross, N.: Algebraic and Logical Methods in Quantum Computation. Ph.D. thesis, Dalhousie University (2015)"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Sanders, J.W., Zuliani, P.: Quantum programming. In: Proc. of MPC 2000 (2000)","DOI":"10.1007\/10722010_6"},{"key":"1_CR50","unstructured":"Schlosshauer, M.: Decoherence and the Quantum-To-Classical Transition. Springer Berlin Heidelberg (2007)"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Selinger, P.: A brief survey of quantum programming languages. In: Proc. of FLOPS 2004 (2004)","DOI":"10.1007\/978-3-540-24754-8_1"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14(4) (2004)","DOI":"10.1017\/S0960129504004256"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. In: Proc. of TLCA (2005)","DOI":"10.1007\/11417170_26"},{"key":"1_CR54","unstructured":"Shor, P.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proc. of FOCS \u201994 (1994)"},{"key":"1_CR55","unstructured":"Skorstengaard, L.: An introduction to logical relations (2019)"},{"key":"1_CR56","unstructured":"Valiron, B.: Automated, parametric gate count of quantum programs (2016), https:\/\/is.gd\/XIm3lh, retrieved on Oct. 15 2023"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R.: Liquidhaskell: Experience with refinement types in the real world. In: Proc. of Haskell \u201914 (2014)","DOI":"10.1145\/2633357.2633366"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell. In: Proc. of ICFP \u201914 (2014)","DOI":"10.1145\/2628136.2628161"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Yamakami, T.: A schematic definition of quantum polynomial time computability. The Journal of Symbolic Logic 85(4) (2020)","DOI":"10.1017\/jsl.2020.45"},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"Yanofsky, N.S., Mannucci, M.A.: Quantum Computing for Computer Scientists. Cambridge University Press, USA, 1st edn. (2008)","DOI":"10.1017\/CBO9780511813887"},{"key":"1_CR61","unstructured":"Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1st edn. (2016)"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"\u00c7i\u00e7ek, E., Garg, D., Acar, U.: Refinement Types for Incremental Computational Complexity. In: Programming Languages and Systems, vol.\u00a09032. Springer Berlin Heidelberg (2015)","DOI":"10.1007\/978-3-662-46669-8_17"},{"key":"1_CR63","doi-asserted-by":"crossref","unstructured":"\u00d6mer, B.: Classical concepts in quantum programming. Int. J. Theor. Phys. 44(7) (2005)","DOI":"10.1007\/s10773-005-7071-x"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57267-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T16:02:38Z","timestamp":1712246558000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57267-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572661","9783031572678"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57267-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}