{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T05:55:47Z","timestamp":1781762147779,"version":"3.54.5"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100008952","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-19-CE48-0010-01"],"award-info":[{"award-number":["ANR-19-CE48-0010-01"]}],"id":[{"id":"10.13039\/501100008952","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":[[2020,1]]},"abstract":"<jats:p>Quantum programming languages permit a hardware independent, high-level description of quantum algorithms. In particular, the quantum \u03bb-calculus is a higher-order language with quantum primitives, mixing quantum data and classical control. Giving satisfactory denotational semantics to the quantum \u03bb-calculus is a challenging problem that has attracted significant interest. In the past few years, both static (the quantum relational model) and dynamic (quantum game semantics) denotational models were given, with matching computational adequacy results. However, no model was known to be fully abstract.<\/jats:p>\n          <jats:p>Our first contribution is a full abstraction result for the games model of the quantum \u03bb-calculus. Full abstraction holds with respect to an observational quotient of strategies, obtained by summing valuations of all states matching a given observable. Our proof method for full abstraction extends a technique recently introduced to prove full abstraction for probabilistic coherence spaces with respect to probabilistic PCF.<\/jats:p>\n          <jats:p>Our second contribution is an interpretation-preserving functor from quantum games to the quantum relational model, extending a long line of work on connecting static and dynamic denotational models. From this, it follows that the quantum relational model is fully abstract as well.<\/jats:p>\n          <jats:p>Altogether, this gives a complete denotational landscape for the semantics of the quantum \u03bb-calculus, with static and dynamic models related by a clean functorial correspondence, and both fully abstract.<\/jats:p>","DOI":"10.1145\/3371131","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Full abstraction for the quantum lambda-calculus"],"prefix":"10.1145","volume":"4","author":[{"given":"Pierre","family":"Clairambault","sequence":"first","affiliation":[{"name":"University of Lyon, France \/ ENS Lyon, France \/ CNRS, France \/ LIP, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marc","family":"de Visme","sequence":"additional","affiliation":[{"name":"University of Lyon, France \/ ENS Lyon, France \/ CNRS, France \/ LIP, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80398-6"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782638"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028007"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_7"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.08.014"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.32"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209187"},{"key":"e_1_2_2_11_1","volume-title":"Games and Strategies as Event Structures. LMCS 13, 3","author":"Castellan Simon","year":"2017","unstructured":"Simon Castellan , Pierre Clairambault , Silvain Rideau , and Glynn Winskel . 2017. Games and Strategies as Event Structures. LMCS 13, 3 ( 2017 ). Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. 2017. Games and Strategies as Event Structures. LMCS 13, 3 (2017)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603141"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.31"},{"key":"e_1_2_2_14_1","volume-title":"Thin Games with Symmetry and Concurrent Hyland-Ong Games. Logical Methods in Computer Science 15, 1","author":"Castellan Simon","year":"2019","unstructured":"Simon Castellan , Pierre Clairambault , and Glynn Winskel . 2019. Thin Games with Symmetry and Concurrent Hyland-Ong Games. Logical Methods in Computer Science 15, 1 ( 2019 ). https:\/\/lmcs.episciences.org\/5248 Simon Castellan, Pierre Clairambault, and Glynn Winskel. 2019. Thin Games with Symmetry and Concurrent Hyland-Ong Games. Logical Methods in Computer Science 15, 1 (2019). https:\/\/lmcs.episciences.org\/5248"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290340"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290345"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.34"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(95)00160-3"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_18"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.01.005"},{"key":"e_1_2_2_21_1","volume-title":"APPSEM 2000","author":"Dybjer Peter","year":"2000","unstructured":"Peter Dybjer and Andrzej Filinski . 2000 . Normalization and Partial Evaluation. In Applied Semantics, International Summer School , APPSEM 2000 , Caminha, Portugal , September 9-15, 2000, Advanced Lectures. 137\u2013192. Peter Dybjer and Andrzej Filinski. 2000. Normalization and Partial Evaluation. In Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures. 137\u2013192."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.11.027"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_2_2_24_1","volume-title":"Quantum cryptography. Reviews of modern physics 74, 1","author":"Gisin Nicolas","year":"2002","unstructured":"Nicolas Gisin , Gr\u00e9goire Ribordy , Wolfgang Tittel , and Hugo Zbinden . 2002. Quantum cryptography. Reviews of modern physics 74, 1 ( 2002 ), 145. Nicolas Gisin, Gr\u00e9goire Ribordy, Wolfgang Tittel, and Hugo Zbinden. 2002. Quantum cryptography. Reviews of modern physics 74, 1 (2002), 145."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782637"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2016.10.010"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80312-3"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00241-9"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.015"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38164-5_13"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.6"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.016"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.07.018"},{"key":"e_1_2_2_38_1","volume-title":"Categorical semantics of linear logic. Panoramas et syntheses 27","author":"Melli\u00e8s Paul-Andr\u00e9","year":"2009","unstructured":"Paul-Andr\u00e9 Melli\u00e8s . 2009. Categorical semantics of linear logic. Panoramas et syntheses 27 ( 2009 ), 15\u2013215. Paul-Andr\u00e9 Melli\u00e8s. 2009. Categorical semantics of linear logic. Panoramas et syntheses 27 (2009), 15\u2013215."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00244-4"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002375"},{"key":"e_1_2_2_43_1","volume-title":"ICALP\u201999 (LNCS)","author":"Power John","unstructured":"John Power and Hayo Thielecke . 1999. Closed Freyd- and kappa-categories . In ICALP\u201999 (LNCS) , Vol. 1644 . Springer . John Power and Hayo Thielecke. 1999. Closed Freyd- and kappa-categories. In ICALP\u201999 (LNCS), Vol. 1644. Springer."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.13"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.018"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005238"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.022"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795293172"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.30"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.022"},{"key":"e_1_2_2_52_1","volume-title":"12th International Colloquium Cali","author":"Winskel Glynn","year":"2015","unstructured":"Glynn Winskel . 2015 . On Probabilistic Distributed Strategies. In Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali , Colombia, October 29-31, 2015, Proceedings. 69\u201388. Glynn Winskel. 2015. On Probabilistic Distributed Strategies. In Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings. 69\u201388."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.02.020"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371131","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371131"],"URL":"https:\/\/doi.org\/10.1145\/3371131","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}