{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T05:55:13Z","timestamp":1781762113631,"version":"3.54.5"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP20H05703"],"award-info":[{"award-number":["JP20H05703"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"name":"ROIS NII Open Collaborative Research","award":["2023-23FA05"],"award-info":[{"award-number":["2023-23FA05"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Selinger gave a superoperator model of a first-order quantum programming language and proved that it is fully definable and hence fully abstract. This paper proposes an extension of the superoperator model to higher-order programs based on modules over superoperators or, equivalently, enriched presheaves over the category of superoperators. The enriched presheaf category can be easily proved to be a model of intuitionistic linear logic with cofree exponential, from which one can cave out a model of classical linear logic by a kind of bi-orthogonality construction. Although the structures of an enriched presheaf category are usually rather complex, a morphism in the classical model can be expressed simply as a matrix of completely positive maps.<\/jats:p>\n          <jats:p>\n            The model inherits many desirable properties from the superoperator model. A conceptually interesting property is that our model has only a state whose \u201ctotal probability\u201d is bounded by 1,\n            <jats:italic toggle=\"yes\">i.e.<\/jats:italic>\n            does not have a state where true and false each occur with probability\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mn>2<\/mml:mn>\n                  <mml:mo>\/<\/mml:mo>\n                  <mml:mn>3<\/mml:mn>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            . Another convenient property inherited from the superoperator model is a\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>\u03c9<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            CPO-enrichment. Remarkably, our model has a sufficient structure to interpret arbitrary recursive types by the standard domain theoretic technique. We introduce\n            <jats:italic toggle=\"yes\">Quantum FPC<\/jats:italic>\n            , a quantum\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>\u03bb<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -calculus with recursive types, and prove that our model is a fully abstract model of Quantum FPC.\n          <\/jats:p>","DOI":"10.1145\/3632855","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"362-392","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Enriched Presheaf Model of Quantum FPC"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"first","affiliation":[{"name":"Chiba University, Chiba, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8782-2119","authenticated-orcid":false,"given":"Kazuyuki","family":"Asada","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.1996.561324"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511600579"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Pablo Andr\u00e9s-Martinez and Chris Heunen. 2023. Categories of sets with infinite addition. (Aug. 2023). https:\/\/doi.org\/10.48550\/ARXIV.2308.15183 10.48550\/ARXIV.2308.15183 arXiv :2308.15183 [math.CT]","DOI":"10.48550\/ARXIV.2308.15183"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511525865"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00354-016-0204-3"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371131"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290345"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/_j.ic.2011.02.001"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0060438"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3164540"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.06.001"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Thomas Ehrhard Christine Tasson and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM. https:\/\/doi.org\/10.1145\/2535838.2535865 10.1145\/2535838.2535865","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.1994.316083"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511526565"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511550850.011"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0960129599003035"},{"key":"e_1_3_1_19_1","volume-title":"Categorical Glueing and Logical Predicates for Models of Linear Logic","author":"Hasegawa Masahito","year":"1999","unstructured":"Masahito Hasegawa. 1999. Categorical Glueing and Logical Predicates for Models of Linear Logic. Technical Report."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2011.26"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/_j.apal.2016.10.010"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_22"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0304-3975(01)00241-9"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498687"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(80)90101-2"},{"key":"e_1_3_1_27_1","first-page":"231","volume-title":"Basic concepts of enriched category theory","author":"Kelly Gregory Maxwell","year":"1982","unstructured":"Gregory Maxwell Kelly. 1982. Basic concepts of enriched category theory. Number 64 in London Mathematical Society lecture note series. Cambridge University Press. Bibliography: p. 231-238."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2013.36"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-17(2:9)2021"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Octavio Malherbe. 2013. Categorical models of computation: partially traced categories and presheaf models of quantum computation. (Jan. 2013). https:\/\/doi.org\/10.48550\/ARXIV.1301.5087 10.48550\/ARXIV.1301.5087 arXiv :1301.5087 [math.CT]","DOI":"10.48550\/ARXIV.1301.5087"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4962-7"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_29"},{"key":"e_1_3_1_34_1","volume-title":"Denotational semantics with partial functions","author":"Plotkin Gordon D.","year":"1985","unstructured":"Gordon D. Plotkin. 1985. Denotational semantics with partial functions. Technical Report."},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.2989\/qm.2008.31.2.2.474"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:30)2020"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0960129504004256"},{"key":"e_1_3_1_38_1","unstructured":"Peter Selinger. 2004b. Towards a semantics for higher-order quantum computation. In Proceedings of the 2nd International Workshop on Quantum Programming Languages. 127\u2013143."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.022"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9781139193313.005"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676999"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533373"},{"key":"e_1_3_1_43_1","doi-asserted-by":"crossref","unstructured":"Takeshi Tsukada and Kazuyuki Asada. 2023. Enriched Presheaf Model of Quantum FPC. (Nov. 2023). arXiv:2311.03117 [cs.PL]","DOI":"10.1145\/3632855"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Takeshi Tsukada Kazuyuki Asada and C.-H. Luke Ong. 2017. Generalised species of rigid resource terms. In 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). IEEE. https:\/\/doi.org\/10.1109\/lics.2017.8005093 10.1109\/lics.2017.8005093","DOI":"10.1109\/lics.2017.8005093"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209157"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2015.30"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934553"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632855","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632855","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:21Z","timestamp":1751659461000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632855"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632855"],"URL":"https:\/\/doi.org\/10.1145\/3632855","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}