{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:53:28Z","timestamp":1767920008861,"version":"3.49.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","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>In this paper, a monad-based denotational model is introduced and shown adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to separate the value to which a term reduces from the circuit 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.<\/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":0,"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"}]},{"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"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_3"},{"key":"e_1_2_1_2_1","volume-title":"RC 2019, Lausanne, Switzerland, June 24-25, 2019, Proceedings, Michael Kirkedal Thomsen and Mathias Soeken (Eds.) (Lecture Notes in Computer Science","volume":"107","author":"Amy Matthew","year":"2019","unstructured":"Matthew Amy. 2019. Sized Types for Low-Level Quantum Metaprogramming. In Reversible Computation - 11th International Conference, RC 2019, Lausanne, Switzerland, June 24-25, 2019, Proceedings, Michael Kirkedal Thomsen and Mathias Soeken (Eds.) (Lecture Notes in Computer Science, Vol. 11497). Springer, 87\u2013107. https:\/\/doi.org\/10.1007\/978-3-030-21500-2_6 10.1007\/978-3-030-21500-2_6"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_2_1_4_1","volume-title":"8th International Workshop, CSL \u201994","volume":"135","author":"Benton P. N.","year":"1994","unstructured":"P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Computer Science Logic, 8th International Workshop, CSL \u201994, Kazimierz, Poland, September 25-30, 1994, Selected Papers, Leszek Pacholski and Jerzy Tiuryn (Eds.) (Lecture Notes in Computer Science, Vol. 933). Springer, 121\u2013135. https:\/\/doi.org\/10.1007\/BFB0022251 10.1007\/BFB0022251"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1140\/epjd\/e2003-00242-2"},{"key":"e_1_2_1_6_1","volume-title":"Von Neumann Algebras form a Model for the Quantum Lambda Calculus. CoRR, abs\/1603.02133","author":"Cho Kenta","year":"2016","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. arxiv:1603.02133"},{"key":"e_1_2_1_7_1","volume-title":"Proc. ACM Program. Lang., 4, POPL","author":"Clairambault Pierre","year":"2020","unstructured":"Pierre Clairambault and Marc de Visme. 2020. Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang., 4, POPL (2020), 63:1\u201363:28. https:\/\/doi.org\/10.1145\/3371131 10.1145\/3371131"},{"key":"e_1_2_1_8_1","volume-title":"Proc. ACM Program. Lang., 3, POPL","author":"Clairambault Pierre","year":"2019","unstructured":"Pierre Clairambault, Marc de Visme, and Glynn Winskel. 2019. Game semantics for quantum programming. Proc. ACM Program. Lang., 3, POPL (2019), 32:1\u201332:29. https:\/\/doi.org\/10.1145\/3290345 10.1145\/3290345"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2022.3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_1"},{"key":"e_1_2_1_11_1","volume-title":"Proc. ACM Program. Lang., 9, POPL","author":"Colledan Andrea","year":"2025","unstructured":"Andrea Colledan and Ugo Dal Lago. 2025. Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages. Proc. ACM Program. Lang., 9, POPL (2025), Article 47, Jan., 31 pages. https:\/\/doi.org\/10.1145\/3704883 10.1145\/3704883"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Lago Ugo Dal","year":"2017","unstructured":"Ugo Dal Lago, Claudia Faggian, Beno\u00eet Valiron, and Akira Yoshimizu. 2017. The geometry of parallelism: classical, probabilistic, and quantum effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 833\u2013845. https:\/\/doi.org\/10.1145\/3009837.3009859 10.1145\/3009837.3009859"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Cirq Developers. 2025. Cirq. https:\/\/doi.org\/10.5281\/zenodo.15191735 10.5281\/zenodo.15191735","DOI":"10.5281\/zenodo.15191735"},{"key":"e_1_2_1_14_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_2_1_15_1","volume-title":"RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings, Ivan Lanese and Mariusz Rawski (Eds.) (Lecture Notes in Computer Science","volume":"168","author":"Fu Peng","year":"2020","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 Reversible Computation - 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings, Ivan Lanese and Mariusz Rawski (Eds.) (Lecture Notes in Computer Science, Vol. 12227). Springer, 153\u2013168. https:\/\/doi.org\/10.1007\/978-3-030-52482-1_9 10.1007\/978-3-030-52482-1_9"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings 19th International Conference on Quantum Physics and Logic, QPL 2022, Wolfson College","volume":"342","author":"Fu Peng","year":"2022","unstructured":"Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2022. 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, Stefano Gogioso and Matty Hoban (Eds.) (EPTCS, Vol. 394). 302\u2013342. https:\/\/doi.org\/10.4204\/EPTCS.394.16 10.4204\/EPTCS.394.16"},{"key":"e_1_2_1_17_1","volume-title":"Proc. ACM Program. Lang., 7, POPL","author":"Fu Peng","year":"2023","unstructured":"Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2023. Proto-Quipper with Dynamic Lifting. Proc. ACM Program. Lang., 7, POPL (2023), 309\u2013334. https:\/\/doi.org\/10.1145\/3571204 10.1145\/3571204"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(3:28)2022"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_9"},{"key":"e_1_2_1_20_1","volume-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913","author":"Green Alexander S.","year":"2013","unstructured":"Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Beno\u00eet Valiron. 2013. Quipper: a scalable quantum programming language. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 333\u2013342. https:\/\/doi.org\/10.1145\/2491956.2462177 10.1145\/2491956.2462177"},{"key":"e_1_2_1_21_1","volume-title":"Proc. ACM Program. Lang., 4, OOPSLA","author":"H\u00e4ner Thomas","year":"2020","unstructured":"Thomas H\u00e4ner, Torsten Hoefler, and Matthias Troyer. 2020. Assertion-based optimization of Quantum programs. Proc. ACM Program. Lang., 4, OOPSLA (2020), 133:1\u2013133:20. https:\/\/doi.org\/10.1145\/3428201 10.1145\/3428201"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.APAL.2016.10.010"},{"key":"e_1_2_1_23_1","volume-title":"Gambetta","author":"Javadi-Abhari Ali","year":"2024","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. arxiv:2405.08810"},{"key":"e_1_2_1_24_1","volume-title":"Proc. ACM Program. Lang., 6, POPL","author":"Jia Xiaodong","year":"2022","unstructured":"Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael W. Mislove, and Vladimir Zamdzhiev. 2022. Semantics for variational Quantum programming. Proc. ACM Program. Lang., 6, POPL (2022), 1\u201331. https:\/\/doi.org\/10.1145\/3498687 10.1145\/3498687"},{"key":"e_1_2_1_25_1","volume-title":"Proc. ACM Program. Lang., 8, PLDI","author":"Jiang Hanru","year":"2024","unstructured":"Hanru Jiang. 2024. Qubit Recycling Revisited. Proc. ACM Program. Lang., 8, PLDI (2024), 1264\u20131287. https:\/\/doi.org\/10.1145\/3656428 10.1145\/3656428"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(91)90003-P"},{"key":"e_1_2_1_27_1","volume-title":"The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914","year":"2014","unstructured":"Shin-ya Katsumata. 2014. Parametric effect monads and semantics of effect systems. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 633\u2013646. https:\/\/doi.org\/10.1145\/2535838.2535846 10.1145\/2535838.2535846"},{"key":"e_1_2_1_28_1","volume-title":"Conventions for Quantum Pseudocode. arxiv:2211","author":"Knill E.","year":"2022","unstructured":"E. Knill. 2022. Conventions for Quantum Pseudocode. arxiv:2211.02559. arxiv:2211.02559 [A version of LANL report LAUR-96-2724 (1996) with a modern formatting]"},{"key":"e_1_2_1_29_1","unstructured":"Paul Blain Levy. 2019. Locally graded categories. https:\/\/pblevy.github.io\/papers\/locgrade.pdf Talk slides"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018","author":"Lindenhovius Bert","year":"2018","unstructured":"Bert Lindenhovius, Michael W. Mislove, and Vladimir Zamdzhiev. 2018. Enriching a Linear\/Non-linear Lambda Calculus: A Programming Language for String Diagrams. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Gr\u00e4del (Eds.). ACM, 659\u2013668. https:\/\/doi.org\/10.1145\/3209108.3209196 10.1145\/3209108.3209196"},{"key":"e_1_2_1_32_1","first-page":"2019","volume-title":"Arch. Formal Proofs","author":"Liu Junyi","year":"2019","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_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Octavio Malherbe Philip J. Scott and Peter Selinger. 2013. Presheaf Models of Quantum Computation: An Outline. In Computation Logic Games and Quantum Foundations. The Many Facets of Samson Abramsky - Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday Bob Coecke Luke Ong and Prakash Panangaden (Eds.) (Lecture Notes in Computer Science Vol. 7860). Springer 178\u2013194. https:\/\/doi.org\/10.1007\/978-3-642-38164-5_13 10.1007\/978-3-642-38164-5_13","DOI":"10.1007\/978-3-642-38164-5_13"},{"key":"e_1_2_1_34_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_2_1_35_1","volume-title":"Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201989)","author":"Moggi Eugenio","year":"1989","unstructured":"Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201989), Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 14\u201323. https:\/\/doi.org\/10.1109\/LICS.1989.39155 10.1109\/LICS.1989.39155"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings Eighth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2020","author":"Orchard Dominic","year":"2020","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, Max S. New and Sam Lindley (Eds.) (EPTCS, Vol. 317). 18\u201338. https:\/\/doi.org\/10.4204\/EPTCS.317.2 10.4204\/EPTCS.317.2"},{"key":"e_1_2_1_38_1","volume-title":"The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914","author":"Pagani Michele","year":"2014","unstructured":"Michele Pagani, Peter Selinger, and Beno\u00eet Valiron. 2014. Applying quantitative semantics to higher-order quantum computing. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 647\u2013658. https:\/\/doi.org\/10.1145\/2535838.2535879 10.1145\/2535838.2535879"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Paykin Jennifer","year":"2017","unstructured":"Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: a core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 846\u2013858. https:\/\/doi.org\/10.1145\/3009837.3009894 10.1145\/3009837.3009894"},{"key":"e_1_2_1_40_1","volume-title":"15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings, Mar\u00eda Alpuente and Germ\u00e1n Vidal (Eds.) (Lecture Notes in Computer Science","volume":"282","author":"Perdrix Simon","year":"2008","unstructured":"Simon Perdrix. 2008. Quantum Entanglement Analysis Based on Abstract Interpretation. In Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings, Mar\u00eda Alpuente and Germ\u00e1n Vidal (Eds.) (Lecture Notes in Computer Science, Vol. 5079). Springer, 270\u2013282. https:\/\/doi.org\/10.1007\/978-3-540-69166-2_18 10.1007\/978-3-540-69166-2_18"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002375"},{"key":"e_1_2_1_42_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_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:30)2020"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017","volume":"178","author":"Rios Francisco","year":"2017","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, Bob Coecke and Aleks Kissinger (Eds.) (EPTCS, Vol. 266). 164\u2013178. https:\/\/doi.org\/10.4204\/EPTCS.266.11 10.4204\/EPTCS.266.11"},{"key":"e_1_2_1_45_1","volume-title":"Logical Methods in Computer Science","volume":"21","author":"Rom\u00e1n Mario","year":"2025","unstructured":"Mario Rom\u00e1n and Pawe\u0142 Soboci\u0144ski. 2025. String Diagrams for Premonoidal Categories. Logical Methods in Computer Science, Volume 21, Issue 2 (2025), Article 9, Apr, issn:1860-5974 https:\/\/doi.org\/10.46298\/lmcs-21(2:9)2025 10.46298\/lmcs-21(2:9)2025"},{"key":"e_1_2_1_46_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. arxiv:2511.22419"},{"key":"e_1_2_1_47_1","unstructured":"J. W. Sanders and P. Zuliani. 2000. Quantum Programming. In Mathematics of Program Construction Roland Backhouse and Jos\u00e9 Nuno Oliveira (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 80\u201399. isbn:978-3-540-45025-2"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_1_49_1","volume-title":"A Lambda Calculus for Quantum Computation with Classical Control","author":"Selinger Peter","year":"2014","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. isbn:978-3-540-32014-2"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 4th International Workshop on Quantum Programming Languages, QPL 2006","author":"Selinger Peter","year":"2008","unstructured":"Peter Selinger and Beno\u00eet Valiron. 2008. On a Fully Abstract Model for a Quantum Linear Functional Language: (Extended Abstract). In Proceedings of the 4th International Workshop on Quantum Programming Languages, QPL 2006, Oxford, UK, July 17-19, 2006, Peter Selinger (Ed.) (Electronic Notes in Theoretical Computer Science, Vol. 210). Elsevier, 123\u2013137. https:\/\/doi.org\/10.1016\/J.ENTCS.2008.04.022 10.1016\/J.ENTCS.2008.04.022"},{"key":"e_1_2_1_51_1","volume-title":"Algorithms for Quantum Computation: Discrete Logarithms and Factoring. In 35th Annual Symposium on Foundations of Computer Science","author":"Shor Peter W.","year":"1994","unstructured":"Peter W. Shor. 1994. Algorithms for Quantum Computation: Discrete Logarithms and Factoring. In 35th Annual Symposium on Foundations of Computer Science, Santa Fe, New Mexico, USA, 20-22 November 1994. IEEE Computer Society, 124\u2013134. https:\/\/doi.org\/10.1109\/SFCS.1994.365700 10.1109\/SFCS.1994.365700"},{"key":"e_1_2_1_52_1","volume-title":"The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913","author":"Staton Sam","year":"2013","unstructured":"Sam Staton and Paul Blain Levy. 2013. Universal properties of impure programming languages. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 179\u2013192. https:\/\/doi.org\/10.1145\/2429069.2429091 10.1145\/2429069.2429091"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the Real World Domain Specific Languages Workshop 2018 (RWDSL2018)","author":"Svore Krysta","year":"2018","unstructured":"Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. 2018. Q#: Enabling Scalable Quantum Computing and Development with a High-level DSL. In Proceedings of the Real World Domain Specific Languages Workshop 2018 (RWDSL2018). ACM. https:\/\/doi.org\/10.1145\/3183895.3183901 10.1145\/3183895.3183901"},{"key":"e_1_2_1_54_1","volume-title":"Proc. ACM Program. Lang., 8, POPL","author":"Tsukada Takeshi","year":"2024","unstructured":"Takeshi Tsukada and Kazuyuki Asada. 2024. Enriched Presheaf Model of Quantum FPC. Proc. ACM Program. Lang., 8, POPL (2024), 362\u2013392. https:\/\/doi.org\/10.1145\/3632855 10.1145\/3632855"},{"key":"e_1_2_1_55_1","volume-title":"RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings, Simon J. Devitt and Ivan Lanese (Eds.) (Lecture Notes in Computer Science","volume":"306","author":"Valiron Beno\u00eet","year":"2016","unstructured":"Beno\u00eet Valiron. 2016. Generating Reversible Circuits from Higher-Order Functional Programs. In Reversible Computation - 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings, Simon J. Devitt and Ivan Lanese (Eds.) (Lecture Notes in Computer Science, Vol. 9720). Springer, 289\u2013306. https:\/\/doi.org\/10.1007\/978-3-319-40578-0_21 10.1007\/978-3-319-40578-0_21"},{"key":"e_1_2_1_56_1","volume-title":"Indexed Categories and Their Applications","author":"Wood R. J.","unstructured":"R. J. Wood. 1978. V-indexed categories. In Indexed Categories and Their Applications. Springer Berlin Heidelberg, Berlin, Heidelberg. 126\u2013140. isbn:978-3-540-35762-9"},{"key":"e_1_2_1_57_1","volume-title":"Foundations of Quantum Programming","author":"Ying Mingsheng","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming (1st ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. isbn:0128023066","edition":"1"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Ying Mingsheng","year":"2017","unstructured":"Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. 2017. Invariants of quantum programs: characterisations and generation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 818\u2013832. https:\/\/doi.org\/10.1145\/3009837.3009840 10.1145\/3009837.3009840"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_20"},{"key":"e_1_2_1_60_1","volume-title":"42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"Yu Nengkun","year":"2021","unstructured":"Nengkun Yu and Jens Palsberg. 2021. Quantum abstract interpretation. In PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.). ACM, 542\u2013558. https:\/\/doi.org\/10.1145\/3453483.3454061 10.1145\/3453483.3454061"},{"key":"e_1_2_1_61_1","volume-title":"Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019","author":"Zhou Li","year":"2019","unstructured":"Li Zhou, Nengkun Yu, and Mingsheng Ying. 2019. An applied quantum Hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 1149\u20131162. https:\/\/doi.org\/10.1145\/3314221.3314584 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,1,8]],"date-time":"2026-01-08T19:06:03Z","timestamp":1767899163000},"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"}}]}}