{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T05:09:26Z","timestamp":1790744966372,"version":"4.1.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-16-1-0082"],"award-info":[{"award-number":["FA9550-16-1-0082"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical\/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.<\/jats:p>","DOI":"10.1145\/3498687","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Semantics for variational Quantum programming"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9310-6143","authenticated-orcid":false,"given":"Xiaodong","family":"Jia","sequence":"first","affiliation":[{"name":"Hunan University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8930-7126","authenticated-orcid":false,"given":"Andre","family":"Kornell","sequence":"additional","affiliation":[{"name":"Tulane University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5380-4705","authenticated-orcid":false,"given":"Bert","family":"Lindenhovius","sequence":"additional","affiliation":[{"name":"JKU Linz, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6650-1399","authenticated-orcid":false,"given":"Michael","family":"Mislove","sequence":"additional","affiliation":[{"name":"Tulane University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9061-3921","authenticated-orcid":false,"given":"Vladimir","family":"Zamdzhiev","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561324"},{"key":"e_1_2_2_2_1","unstructured":"S. Abramsky and A. Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science (Vol. 3). Oxford University Press Oxford UK. 1\u2013168. isbn:0-19-853762-X http:\/\/dl.acm.org\/citation.cfm?id=218742.218744  S. Abramsky and A. Jung. 1994. Domain Theory. In Handbook of Logic in Computer Science (Vol. 3). Oxford University Press Oxford UK. 1\u2013168. isbn:0-19-853762-X http:\/\/dl.acm.org\/citation.cfm?id=218742.218744"},{"key":"e_1_2_2_3_1","volume-title":"Wootters","author":"Bennett Charles H.","year":"1993","unstructured":"Charles H. Bennett , Gilles Brassard , Claude Cr\u00e9peau , Richard Jozsa , Asher Peres , and William K . Wootters . 1993 . Teleporting an Unknown Quantum State via Dual Classical and EPR Channels . Charles H. Bennett, Gilles Brassard, Claude Cr\u00e9peau, Richard Jozsa, Asher Peres, and William K. Wootters. 1993. Teleporting an Unknown Quantum State via Dual Classical and EPR Channels."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022251"},{"key":"e_1_2_2_5_1","volume-title":"Monads and the Lambda Calculus. In LICS","author":"Benton P. N.","year":"1996","unstructured":"P. N. Benton and P. Wadler . 1996. Linear Logic , Monads and the Lambda Calculus. In LICS 1996 . P. N. Benton and P. Wadler. 1996. Linear Logic, Monads and the Lambda Calculus. In LICS 1996."},{"key":"e_1_2_2_6_1","volume-title":"Operator Algebras: Theory of C*-algebras and von Neumann algebras","author":"Blackadar B.","unstructured":"B. Blackadar . 2006. Operator Algebras: Theory of C*-algebras and von Neumann algebras . Springer-Verlag . B. Blackadar. 2006. Operator Algebras: Theory of C*-algebras and von Neumann algebras. Springer-Verlag."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00354-016-0204-3"},{"key":"e_1_2_2_8_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 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_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371131"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290345"},{"key":"e_1_2_2_11_1","unstructured":"Edward Farhi Jeffrey Goldstone and Sam Gutmann. 2014. A Quantum Approximate Optimization Algorithm. arxiv:1411.4028.  Edward Farhi Jeffrey Goldstone and Sam Gutmann. 2014. A Quantum Approximate Optimization Algorithm. arxiv:1411.4028."},{"key":"e_1_2_2_12_1","volume-title":"An Axiomatization of Computationally Adequate Domain Theoretic Models of FPC","author":"Fiore Marcelo","unstructured":"Marcelo Fiore and Gordon Plotkin . 1994. An Axiomatization of Computationally Adequate Domain Theoretic Models of FPC . In LICS. IEEE Computer Society , 92\u2013102. Marcelo Fiore and Gordon Plotkin. 1994. An Axiomatization of Computationally Adequate Domain Theoretic Models of FPC. In LICS. IEEE Computer Society, 92\u2013102."},{"key":"e_1_2_2_14_1","unstructured":"R. Furber. 2019. Continuous Dcpos in Quantum Computing. preprint http:\/\/people.cs.aau.dk\/~furber\/papers\/contawconf.pdf  R. Furber. 2019. Continuous Dcpos in Quantum Computing. preprint http:\/\/people.cs.aau.dk\/~furber\/papers\/contawconf.pdf"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"G. Gierz K. H. Hofmann K. Keimel J. D. Lawson M. W. Mislove and D. S. Scott. 2003. Continuous Lattices and Domains. Cambridge University Press.  G. Gierz K. H. Hofmann K. Keimel J. D. Lawson M. W. Mislove and D. S. Scott. 2003. Continuous Lattices and Domains. Cambridge University Press.","DOI":"10.1017\/CBO9780511542725"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_17_1","volume-title":"Practical Foundations for Programming Languages (2nd. Ed.)","author":"Harper Robert","unstructured":"Robert Harper . 2016. Practical Foundations for Programming Languages (2nd. Ed.) . Cambridge University Press . isbn:9781107150300 https:\/\/www.cs.cmu.edu\/%7Erwh\/pfpl\/index.html Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press. isbn:9781107150300 https:\/\/www.cs.cmu.edu\/%7Erwh\/pfpl\/index.html"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_2_2_19_1","volume-title":"Semantics for Variational Quantum Programming. CoRR, abs\/2107.13347","author":"Jia Xiaodong","year":"2021","unstructured":"Xiaodong Jia , Andre Kornell , Bert Lindenhovius , Michael W. Mislove , and Vladimir Zamdzhiev . 2021. Semantics for Variational Quantum Programming. CoRR, abs\/2107.13347 ( 2021 ), arXiv:2107.13347. arxiv:2107.13347 Extended version of this POPL paper. Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael W. Mislove, and Vladimir Zamdzhiev. 2021. Semantics for Variational Quantum Programming. CoRR, abs\/2107.13347 (2021), arXiv:2107.13347. arxiv:2107.13347 Extended version of this POPL paper."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470611"},{"key":"e_1_2_2_21_1","volume-title":"The Central Valuations Monad. CoRR, abs\/2111.10873","author":"Jia Xiaodong","year":"2021","unstructured":"Xiaodong Jia , Michael W. Mislove , and Vladimir Zamdzhiev . 2021. The Central Valuations Monad. CoRR, abs\/2111.10873 ( 2021 ), arXiv:2111.10873. arxiv:2111.10873 Xiaodong Jia, Michael W. Mislove, and Vladimir Zamdzhiev. 2021. The Central Valuations Monad. CoRR, abs\/2111.10873 (2021), arXiv:2111.10873. arxiv:2111.10873"},{"key":"e_1_2_2_22_1","unstructured":"Claire Jones. 1990. Probabilistic Non-determinism. Ph.D. Dissertation. University of Edinburgh UK. http:\/\/hdl.handle.net\/1842\/413  Claire Jones. 1990. Probabilistic Non-determinism. Ph.D. Dissertation. University of Edinburgh UK. http:\/\/hdl.handle.net\/1842\/413"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39173"},{"key":"e_1_2_2_24_1","volume-title":"Elementary Theory","author":"Kadison R.V.","year":"1997","unstructured":"R.V. Kadison and J.R. Ringrose . 1997 . Fundamentals of the Theory of Operator Algebra , Volume I : Elementary Theory . American Mathematical Society . R.V. Kadison and J.R. Ringrose. 1997. Fundamentals of the Theory of Operator Algebra, Volume I: Elementary Theory. American Mathematical Society."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:2)2017"},{"key":"e_1_2_2_26_1","unstructured":"John L. Kelley. 1975. General Topology (Graduate Texts in Mathematics). Springer-Verlag. issn:978-0-387-90125-1  John L. Kelley. 1975. General Topology (Graduate Texts in Mathematics). Springer-Verlag. issn:978-0-387-90125-1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.5054128"},{"key":"e_1_2_2_28_1","volume-title":"Foundations of Quantum Theory - From Classical Concepts to Operator Algebras","author":"Landsman Klaas","unstructured":"Klaas Landsman . 2017. Foundations of Quantum Theory - From Classical Concepts to Operator Algebras . Springer Open . Klaas Landsman. 2017. Foundations of Quantum Theory - From Classical Concepts to Operator Algebras. Springer Open."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341715"},{"key":"e_1_2_2_30_1","volume-title":"Logical Methods in Computer Science","volume":"17","author":"Lindenhovius Bert","year":"2021","unstructured":"Bert Lindenhovius , Michael Mislove , and Vladimir Zamdzhiev . 2021 . LNL-FPC: The Linear\/Non-linear Fixpoint Calculus . Logical Methods in Computer Science , Volume 17 , Issue 2 (2021), April, https:\/\/lmcs.episciences.org\/7390 Bert Lindenhovius, Michael Mislove, and Vladimir Zamdzhiev. 2021. LNL-FPC: The Linear\/Non-linear Fixpoint Calculus. Logical Methods in Computer Science, Volume 17, Issue 2 (2021), April, https:\/\/lmcs.episciences.org\/7390"},{"key":"e_1_2_2_31_1","volume-title":"Categories for the Working Mathematician","author":"Lane Saunders Mac","unstructured":"Saunders Mac Lane . 1998. Categories for the Working Mathematician ( 2 nd ed.). Springer . Saunders Mac Lane. 1998. Categories for the Working Mathematician (2nd ed.). Springer.","edition":"2"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/18\/2\/023023"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_34_1","first-page":"15","article-title":"Repeat-until-Success","volume":"14","author":"Paetznick Adam","year":"2014","unstructured":"Adam Paetznick and Krysta M. Svore . 2014 . Repeat-until-Success : Non-Deterministic Decomposition of Single-Qubit Unitaries. Quantum Info. Comput. , 14 , 15 \u2013 16 (2014), Nov., 1277\u20131301. issn:1533-7146 Adam Paetznick and Krysta M. Svore. 2014. Repeat-until-Success: Non-Deterministic Decomposition of Single-Qubit Unitaries. Quantum Info. Comput., 14, 15\u201316 (2014), Nov., 1277\u20131301. issn:1533-7146","journal-title":"Non-Deterministic Decomposition of Single-Qubit Unitaries. Quantum Info. Comput."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"J. Paykin R. Rand and S. Zdancewic. 2017. QWIRE: a core language for quantum circuits. In POPL. ACM 846\u2013858.  J. Paykin R. Rand and S. Zdancewic. 2017. QWIRE: a core language for quantum circuits. In POPL. ACM 846\u2013858.","DOI":"10.1145\/3093333.3009894"},{"key":"e_1_2_2_37_1","unstructured":"Romain P\u00e9choux Simon Perdrix Mathys Rennela and Vladimir Zamdzhiev. 2020. Quantum Programming with Inductive Datatypes. https:\/\/homepages.loria.fr\/VZamdzhiev\/papers\/qpl-inductive.pdf Preprint.  Romain P\u00e9choux Simon Perdrix Mathys Rennela and Vladimir Zamdzhiev. 2020. Quantum Programming with Inductive Datatypes. https:\/\/homepages.loria.fr\/VZamdzhiev\/papers\/qpl-inductive.pdf Preprint."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_29"},{"key":"e_1_2_2_39_1","volume-title":"A variational eigenvalue solver on a photonic quantum processor. Nature communications, 5, 1","author":"Peruzzo Alberto","year":"2014","unstructured":"Alberto Peruzzo , Jarrod McClean , Peter Shadbolt , Man-Hong Yung , Xiao-Qi Zhou , Peter J Love , Al\u00e1n Aspuru-Guzik , and Jeremy L O\u2019brien . 2014. A variational eigenvalue solver on a photonic quantum processor. Nature communications, 5, 1 ( 2014 ), 1\u20137. Alberto Peruzzo, Jarrod McClean, Peter Shadbolt, Man-Hong Yung, Xiao-Qi Zhou, Peter J Love, Al\u00e1n Aspuru-Guzik, and Jeremy L O\u2019brien. 2014. A variational eigenvalue solver on a photonic quantum processor. Nature communications, 5, 1 (2014), 1\u20137."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002375"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:30)2020"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_2_43_1","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages, 127\u2013143","author":"Selinger Peter","year":"2004","unstructured":"Peter Selinger . 2004 . Towards a semantics for higher-order quantum computation . Proceedings of the 2nd International Workshop on Quantum Programming Languages, 127\u2013143 . Peter Selinger. 2004. Towards a semantics for higher-order quantum computation. Proceedings of the 2nd International Workshop on Quantum Programming Languages, 127\u2013143."},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","unstructured":"M.B. Smyth and G.D. Plotkin. 1982. The Category-theoretic Solution of Recursive Domain Equations. Siam J. Comput..  M.B. Smyth and G.D. Plotkin. 1982. The Category-theoretic Solution of Recursive Domain Equations. Siam J. Comput..","DOI":"10.1137\/0211062"},{"key":"e_1_2_2_45_1","volume-title":"Theory of Operator Algebra I","author":"Takesaki M.","unstructured":"M. Takesaki . 2000. Theory of Operator Algebra I . Springer . M. Takesaki. 2000. Theory of Operator Algebra I. Springer."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209157"},{"key":"e_1_2_2_48_1","volume-title":"A single quantum cannot be cloned. Nature, 299, 5886","author":"Wootters William K","year":"1982","unstructured":"William K Wootters and Wojciech H Zurek . 1982. A single quantum cannot be cloned. Nature, 299, 5886 ( 1982 ), 802\u2013803. William K Wootters and Wojciech H Zurek. 1982. A single quantum cannot be cloned. Nature, 299, 5886 (1982), 802\u2013803."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498687","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498687","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498687","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498687"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498687"],"URL":"https:\/\/doi.org\/10.1145\/3498687","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}