{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T01:47:55Z","timestamp":1787017675053,"version":"build-2736575974"},"reference-count":61,"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":[{"name":"European Union - NextGenerationEU through the Italian Ministry of University and Research under PNRR","award":["P2022HXNS"],"award-info":[{"award-number":["P2022HXNS"]}]},{"name":"European Union - NextGenerationEU through the Italian Ministry of University and Research under PNRR","award":["CN00000013"],"award-info":[{"award-number":["CN00000013"]}]}],"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                    In this paper, a monad-based denotational model is introduced and shown adequate for the\n                    <jats:monospace>Proto-Quipper<\/jats:monospace>\n                    family of calculi, themselves being idealized versions of the\n                    <jats:monospace>Quipper<\/jats:monospace>\n                    programming language. The use of a monadic approach allows us to separate the\n                    <jats:italic toggle=\"yes\">value<\/jats:italic>\n                    to which a term reduces from the\n                    <jats:italic toggle=\"yes\">circuit<\/jats:italic>\n                    that the term itself produces as a side effect. In turn, this enables the denotational interpretation and validation of rich type systems in which the size of the produced circuit can be controlled. Notably, the proposed semantic framework, through the novel concept of circuit algebra, suggests forms of effect typing guaranteeing quantitative properties about the resulting circuit, even in presence of optimizations.\n                  <\/jats:p>","DOI":"10.1145\/3776666","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"688-717","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["On Circuit Description Languages, Indexed Monads, and Resource Analysis"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3238-9279","authenticated-orcid":false,"given":"Ken","family":"Sakayori","sequence":"first","affiliation":[{"name":"University of Tokyo, Tokyo, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0049-0391","authenticated-orcid":false,"given":"Andrea","family":"Colledan","sequence":"additional","affiliation":[{"name":"University of Bologna, Bologna, Italy"},{"name":"Centre Inria d\u2019Universit\u00e9 C\u00f4te d\u2019Azur, 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":"Centre Inria d\u2019Universit\u00e9 C\u00f4te d\u2019Azur, Valbonne, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_3"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-21500-2_6"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0022251"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1140\/epjd\/e2003-00242-2"},{"key":"e_1_3_2_7_1","unstructured":"Kenta Cho and Abraham Westerbaan. 2016. Von Neumann Algebras form a Model for the Quantum Lambda Calculus. CoRR abs\/1603.02133 (2016). arXiv:1603.02133 http:\/\/arxiv.org\/abs\/1603.02133"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371131"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290345"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2022.3"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_1"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704883"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009859"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"Cirq Developers. 2025. Cirq. doi:10.5281\/zenodo.15191735","DOI":"10.5281\/zenodo.15191735"},{"key":"e_1_3_2_15_1","unstructured":"Conal Elliott. 2013. Circuits as a bicartesian closed category. http:\/\/conal.net\/blog\/posts\/circuits-as-a-bicartesian-closed-category . Blog post Accessed: 2025-01-23."},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-52482-1_9"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Peng Fu Kohei Kishida Neil J. Ross and Peter Selinger. 2022b. A biset-enriched categorical model for Proto-Quipper with dynamic lifting. In Proceedings 19th International Conference on Quantum Physics and Logic QPL 2022 Wolfson College Oxford UK 27 June -1 July 2022 (EPTCS Vol. 394) Stefano Gogioso and Matty Hoban (Eds.). 302\u2013342. doi:10.4204\/EPTCS.394.16","DOI":"10.4204\/EPTCS.394.16"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571204"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(3:28)2022"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_9"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428201"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.APAL.2016.10.010"},{"key":"e_1_3_2_24_1","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 [quant-ph] https:\/\/arxiv.org\/abs\/2405.08810"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498687"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656428"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(91)90003-P"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_2_29_1","unstructured":"E. Knill. 2022. Conventions for Quantum Pseudocode. arXiv:2211.02559 [quant-ph] https:\/\/arxiv.org\/abs\/2211.02559 [A version of LANL report LAUR-96-2724 (1996) with a modern formatting]."},{"key":"e_1_3_2_30_1","unstructured":"Paul Blain Levy. 2019. Locally graded categories. https:\/\/pblevy.github.io\/papers\/locgrade.pdf. Talk slides."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209196"},{"key":"e_1_3_2_33_1","unstructured":"Junyi Liu Bohua Zhan Shuling Wang Shenggang Ying Tao Liu Yangjia Li Mingsheng Ying and Naijun Zhan. 2019. Quantum Hoare Logic. Arch. Formal Proofs 2019 (2019). https:\/\/www.isa-afp.org\/entries\/QHLProver.html"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38164-5_13"},{"key":"e_1_3_2_35_1","unstructured":"Paul-Andr\u00e9 Mellies. 2012. Parametric monads and enriched adjunctions. https:\/\/www.irif.fr\/~mellies\/tensorial-logic\/8-parametric-monads-and-enriched-adjunctions.pdf. Preprint."},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Dominic Orchard Philip Wadler and Harley Eades III. 2020. Unifying graded and parameterised monads. In Proceedings Eighth Workshop on Mathematically Structured Functional Programming MSFP@ETAPS 2020 Dublin Ireland 25th April 2020 (EPTCS Vol. 317) Max S. New and Sam Lindley (Eds.). 18\u201338. doi:10.4204\/EPTCS.317.2","DOI":"10.4204\/EPTCS.317.2"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002375"},{"key":"e_1_3_2_43_1","unstructured":"Qiskit API reference. 2025. HoareOptimizer. https:\/\/quantum.cloud.ibm.com\/docs\/en\/api\/qiskit\/qiskit.transpiler.passes.HoareOptimizer. Accessed: 2025-07-10."},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:30)2020"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Francisco Rios and Peter Selinger. 2017. A categorical model for a quantum circuit description language. In Proceedings 14th International Conference on Quantum Physics and Logic QPL 2017 Nijmegen The Netherlands 3-7 July 2017 (EPTCS Vol. 266) Bob Coecke and Aleks Kissinger (Eds.). 164\u2013178. doi:10.4204\/EPTCS.266.11","DOI":"10.4204\/EPTCS.266.11"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-21(2:9)2025"},{"key":"e_1_3_2_47_1","unstructured":"Ken Sakayori Andrea Colledan and Ugo Dal Lago. 2025. On Circuit Description Languages Indexed Monads and Resource Analysis (Extended Version). arXiv:2511.22419 [cs.PL] https:\/\/arxiv.org\/abs\/2511.22419"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_6"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_50_1","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1007\/11417170_26","volume-title":"Typed Lambda Calculi and Applications","author":"Selinger Peter","year":"2005","unstructured":"Peter Selinger and Beno\u00eet Valiron. 2005. A Lambda Calculus for Quantum Computation with Classical Control. In Typed Lambda Calculi and Applications, Pawe\u0142 Urzyczyn (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 354\u2013368."},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2008.04.022"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429091"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632855"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40578-0_21"},{"key":"e_1_3_2_57_1","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/BFb0061362","volume-title":"Indexed Categories and Their Applications","author":"Wood R. J.","year":"1978","unstructured":"R. J. Wood. 1978. V-indexed categories. In Indexed Categories and Their Applications. Springer Berlin Heidelberg, Berlin, Heidelberg, 126\u2013140."},{"key":"e_1_3_2_58_1","volume-title":"Foundations of Quantum Programming","author":"Ying Mingsheng","year":"2016","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming (1st ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.","edition":"1"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009840"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_20"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776666","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:45:14Z","timestamp":1784209514000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776666"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776666"],"URL":"https:\/\/doi.org\/10.1145\/3776666","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-09","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"}}]}}