{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:43Z","timestamp":1750306783341,"version":"3.41.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,8,1]],"date-time":"2013-08-01T00:00:00Z","timestamp":1375315200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/HO23097"],"award-info":[{"award-number":["EP\/HO23097"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2013,8]]},"abstract":"<jats:p>\n            This article presents a game semantics for higher-rank polymorphism, leading to a new model of the calculus System F, and a programming language which extends it with mutable variables. In contrast to previous game models of polymorphism, it is quite concrete, extending existing categories of games by a simple development of the notion of\n            <jats:italic>question\/answer labelling<\/jats:italic>\n            and the associated\n            <jats:italic>bracketing condition<\/jats:italic>\n            to represent \u201ccopycat links\u201d between positive and negative occurrences of type variables. Some well-known System F encodings of type constructors correspond in our model to simple constructions on games, such as the lifted sum.\n          <\/jats:p>\n          <jats:p>\n            We characterize the\n            <jats:italic>generic<\/jats:italic>\n            types of our model (those for which instantiation reflects denotational equivalence), and show how to construct an interpretation in which all types are generic. We show how mutable variables (\u00e0 la Scheme) may be interpreted in our model, allowing the definition of polymorphic objects with local state. By proving definability of finitary elements in this model using a decomposition argument, we establish a full abstraction result.\n          <\/jats:p>","DOI":"10.1145\/2508028.2505986","type":"journal-article","created":{"date-parts":[[2013,9,3]],"date-time":"2013-09-03T11:57:11Z","timestamp":1378209431000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Game semantics for a polymorphic programming language"],"prefix":"10.1145","volume":"60","author":[{"given":"J.","family":"Laird","sequence":"first","affiliation":[{"name":"University of Bath, Bath, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,9,4]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.5555\/788020.788891"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.2307\/2275407"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1016\/j.apal.2004.10.002"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1006\/inco.2000.2930"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1006\/inco.1994.1013"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.5555\/3266641.3266650"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1109\/LICS.2009.30"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1016\/S0304-3975(03)00315-3"},{"unstructured":"Girard J.-Y. 1972. Interpr\u00e9tation functionelle et elimination des coupures de l'arithm\u00e8tique d'ordre sup\u00e9rieur. Ph.D. thesis Universit\u00e9 Paris VII.  Girard J.-Y. 1972. Interpr\u00e9tation functionelle et elimination des coupures de l'arithm\u00e8tique d'ordre sup\u00e9rieur. Ph.D. thesis Universit\u00e9 Paris VII.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.5555\/788019.788861"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1006\/inco.2000.2917"},{"volume-title":"Proceedings of CTCS'02","year":"2002","author":"Laird J.","key":"e_1_2_1_12_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1109\/LICS.2010.32"},{"volume-title":"Proceedings of ICALP'10","author":"Laird J.","series-title":"Lecture Notes in Computer Science","key":"e_1_2_1_14_1"},{"doi-asserted-by":"crossref","unstructured":"Levy P. B. 2004. Call-By-Push-Value. Semantic Structures in Computation. Kluwer.  Levy P. B. 2004. Call-By-Push-Value. Semantic Structures in Computation. Kluwer.","key":"e_1_2_1_15_1","DOI":"10.1007\/978-94-007-0954-6"},{"volume-title":"Proceedings of LISM'97","author":"Lincoln P. D.","key":"e_1_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1016\/0304-3975(93)90093-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1016\/j.jpaa.2012.03.026"},{"unstructured":"McCusker G. 1996. Games and full abstraction for a functional metalanguage with recursive types. Ph.D. dissertation Imperial College London. Published by Cambridge University Press.  McCusker G. 1996. Games and full abstraction for a functional metalanguage with recursive types. Ph.D. dissertation Imperial College London. Published by Cambridge University Press.","key":"e_1_2_1_19_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.2168\/LMCS-5(3:7)2009"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of CTCS'88","volume":"283","author":"Pitts A.","year":"1988"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.5555\/647323.721503"},{"key":"e_1_2_1_23_1","first-page":"513","article-title":"Types, abstraction and parametric polymorphism","volume":"83","author":"Reynolds J. C.","year":"1983","journal-title":"Inf. Proc."},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.2307\/2273831"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2508028.2505986","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2508028.2505986","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:09Z","timestamp":1750232049000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2508028.2505986"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["10.1145\/2508028.2505986"],"URL":"https:\/\/doi.org\/10.1145\/2508028.2505986","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2013,8]]},"assertion":[{"value":"2011-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-09-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}