{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T20:08:01Z","timestamp":1776715681489,"version":"3.51.2"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"name":"AFOSR","award":["FA9550-21-1-0041"],"award-info":[{"award-number":["FA9550-21-1-0041"]}]},{"name":"NSERC","award":["RGPIN\/05161-17"],"award-info":[{"award-number":["RGPIN\/05161-17"]}]},{"name":"nserc","award":["RGPIN\/04064-2018"],"award-info":[{"award-number":["RGPIN\/04064-2018"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>\n            Quipper is a functional programming language for quantum computing. Proto-Quipper is a family of languages aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a construct called\n            <jats:italic>dynamic lifting<\/jats:italic>\n            , which is present in Quipper. By virtue of being a circuit description language, Proto-Quipper has two separate runtimes: circuit generation time and circuit execution time. Values that are known at circuit generation time are called\n            <jats:italic>parameters<\/jats:italic>\n            , and values that are known at circuit execution time are called\n            <jats:italic>states<\/jats:italic>\n            . Dynamic lifting is an operation that enables a state, such as the result of a measurement, to be lifted to a parameter, where it can influence the generation of the next portion of the circuit. As a result, dynamic lifting enables Proto-Quipper programs to interleave classical and quantum computation. We describe the syntax of a language we call Proto-Quipper-Dyn. Its type system uses a system of modalities to keep track of the use of dynamic lifting. We also provide an operational semantics, as well as an abstract categorical semantics for dynamic lifting based on enriched category theory. We prove that both the type system and the operational semantics are sound with respect to our categorical semantics. Finally, we give some examples of Proto-Quipper-Dyn programs that make essential use of dynamic lifting.\n          <\/jats:p>","DOI":"10.1145\/3571204","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"309-334","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Proto-Quipper with Dynamic Lifting"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3123-0867","authenticated-orcid":false,"given":"Peng","family":"Fu","sequence":"first","affiliation":[{"name":"Dalhousie University, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6719-1521","authenticated-orcid":false,"given":"Kohei","family":"Kishida","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0941-4333","authenticated-orcid":false,"given":"Neil J.","family":"Ross","sequence":"additional","affiliation":[{"name":"Dalhousie University, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3161-856X","authenticated-orcid":false,"given":"Peter","family":"Selinger","sequence":"additional","affiliation":[{"name":"Dalhousie University, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022251"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386007"},{"key":"e_1_2_1_3_1","volume-title":"Handbook of Categorical Algebra, Volume 2: Categories and Structures","author":"Borceux Francis","unstructured":"Francis Borceux . 1994. Handbook of Categorical Algebra, Volume 2: Categories and Structures . Cambridge University Press . Francis Borceux. 1994. Handbook of Categorical Algebra, Volume 2: Categories and Structures. Cambridge University Press."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.71.022316"},{"key":"e_1_2_1_5_1","unstructured":"Andrea Colledan and Ugo Dal Lago. 2022. On dynamic lifting and effect typing in circuit description languages (extended version). Available from 2202.07636 \t\t\t\t  Andrea Colledan and Ugo Dal Lago. 2022. On dynamic lifting and effect typing in circuit description languages (extended version). Available from 2202.07636"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-52482-1_9"},{"key":"e_1_2_1_7_1","volume-title":"To appear in QPL","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. April , To appear in QPL 2022 . Available from 2204.13039 Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2022. A biset-enriched categorical model for Proto-Quipper with dynamic lifting. April, To appear in QPL 2022. Available from 2204.13039"},{"key":"e_1_2_1_8_1","unstructured":"Peng Fu Kohei Kishida Neil J. Ross and Peter Selinger. 2022. Proto-Quipper with dynamic lifting. Available from 2204.13041 \t\t\t\t  Peng Fu Kohei Kishida Neil J. Ross and Peter Selinger. 2022. Proto-Quipper with dynamic lifting. Available from 2204.13041"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394765"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38986-3_10"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462177"},{"key":"e_1_2_1_12_1","unstructured":"G. M. Kelly. 1982. Basic concepts of enriched category theory (Lecture Notes of the London Mathematical Society Vol. 64). Cambridge University Press. \t\t\t\t  G. M. Kelly. 1982. Basic concepts of enriched category theory (Lecture Notes of the London Mathematical Society Vol. 64). Cambridge University Press."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2021.51"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209196"},{"key":"e_1_2_1_15_1","unstructured":"2020. MetaOCaml \u2013 an OCaml dialect for multi-stage programming. https:\/\/okmij.org\/ftp\/ML\/MetaOCaml.html Accessed: 2022-10-05 \t\t\t\t  2020. MetaOCaml \u2013 an OCaml dialect for multi-stage programming. https:\/\/okmij.org\/ftp\/ML\/MetaOCaml.html Accessed: 2022-10-05"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_17_1","volume-title":"Chuang","author":"Nielsen Michael A.","year":"2002","unstructured":"Michael A. Nielsen and Isaac L . Chuang . 2002 . Quantum Computation and Quantum Information. Cambridge University Press . Michael A. Nielsen and Isaac L. Chuang. 2002. Quantum Computation and Quantum Information. Cambridge University Press."},{"key":"e_1_2_1_18_1","volume-title":"A Procedural Formalism for Quantum Computing. Master\u2019s thesis. Department of Theoretical Physics","author":"\u00d6mer Bernhard","unstructured":"Bernhard \u00d6mer . 1998. A Procedural Formalism for Quantum Computing. Master\u2019s thesis. Department of Theoretical Physics , Technical University of Vienna . http:\/\/tph.tuwien.ac.at\/~oemer\/qcl.html Bernhard \u00d6mer. 1998. A Procedural Formalism for Quantum Computing. Master\u2019s thesis. Department of Theoretical Physics, Technical University of Vienna. http:\/\/tph.tuwien.ac.at\/~oemer\/qcl.html"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.26421\/QIC14.15-16-2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:30)2020"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.266.11"},{"key":"e_1_2_1_24_1","volume-title":"Algebraic and logical methods in quantum computation. Ph. D. Dissertation","author":"Ross Neil J.","unstructured":"Neil J. Ross . 2015. Algebraic and logical methods in quantum computation. Ph. D. Dissertation . Dalhousie University , Department of Mathematics and Statistics. Available from 1510.02198 Neil J. Ross. 2015. Algebraic and logical methods in quantum computation. Ph. D. Dissertation. Dalhousie University, Department of Mathematics and Statistics. Available from 1510.02198"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_1_26_1","volume-title":"Semantic Techniques in Quantum Computation","author":"Selinger Peter","unstructured":"Peter Selinger and Beno\u00eet Valiron . 2009. Quantum lambda calculus . In Semantic Techniques in Quantum Computation , Simon Gay and Ian Mackie (Eds.). Cambridge University Press , 135\u2013172. Peter Selinger and Beno\u00eet Valiron. 2009. Quantum lambda calculus. In Semantic Techniques in Quantum Computation, Simon Gay and Ian Mackie (Eds.). Cambridge University Press, 135\u2013172."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571204","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571204","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571204"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":27,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571204"],"URL":"https:\/\/doi.org\/10.1145\/3571204","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}