{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:13Z","timestamp":1747173433013,"version":"3.40.5"},"reference-count":48,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2020,12,18]],"date-time":"2020-12-18T00:00:00Z","timestamp":1608249600000},"content-version":"unspecified","delay-in-days":108,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The present work achieves a mathematical, in particular<jats:italic>syntax-independent<\/jats:italic>, formulation of<jats:italic>dynamics<\/jats:italic>and<jats:italic>intensionality<\/jats:italic>of computation in terms of<jats:italic>games<\/jats:italic>and<jats:italic>strategies<\/jats:italic>. Specifically, we give<jats:italic>game semantics<\/jats:italic>of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the<jats:italic>hiding operation<\/jats:italic>on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a<jats:italic>cartesian closed bicategory<\/jats:italic>, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.<\/jats:p>","DOI":"10.1017\/s0960129520000250","type":"journal-article","created":{"date-parts":[[2020,12,18]],"date-time":"2020-12-18T10:03:46Z","timestamp":1608285826000},"page":"892-951","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Dynamic game semantics"],"prefix":"10.1017","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1253-8943","authenticated-orcid":false,"given":"Norihiro","family":"Yamada","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3921-6637","authenticated-orcid":false,"given":"Samson","family":"Abramsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2020,12,18]]},"reference":[{"volume-title":"Semantics of Programming Languages: Structures and Techniques","year":"1992","author":"Gunter","key":"S0960129520000250_ref26"},{"key":"S0960129520000250_ref30","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"S0960129520000250_ref7","volume-title":"The Lambda Calculus","volume":"3","author":"Barendregt","year":"1984"},{"key":"S0960129520000250_ref1","first-page":"1","volume-title":"Semantics and Logics of Computation","author":"Abramsky","year":"1997"},{"key":"S0960129520000250_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0615-9"},{"volume-title":"Game Semantics for Region Analysis","year":"2005","author":"Greenland","key":"S0960129520000250_ref25"},{"volume-title":"Head linear reduction","year":"2004","author":"Danos","key":"S0960129520000250_ref13"},{"key":"S0960129520000250_ref28","unstructured":"Harmer, R. (2004). Innocent game semantics. In: Lecture Notes, 2007."},{"key":"S0960129520000250_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00392-X"},{"key":"S0960129520000250_ref46","first-page":"65","volume-title":"Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science","author":"Seely","year":"1987"},{"key":"S0960129520000250_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_9"},{"key":"S0960129520000250_ref44","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"S0960129520000250_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.016"},{"key":"S0960129520000250_ref32","volume-title":"Categorical Logic and Type Theory","volume":"141","author":"Jacobs","year":"1999"},{"key":"S0960129520000250_ref2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"S0960129520000250_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511542725"},{"volume-title":"Explicit Substitution: Tutorial and Survey","year":"1996","author":"Rose","key":"S0960129520000250_ref43"},{"volume-title":"A Two-Dimensional Extension of Lambek\u2019s Categorical Proof Theory","year":"1997","author":"Ouaknine","key":"S0960129520000250_ref40"},{"key":"S0960129520000250_ref27","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538417.001.0001","volume-title":"Lambda Calculi: A Guide for computer scientists","volume":"3","author":"Hankin","year":"1994"},{"key":"S0960129520000250_ref21","first-page":"76","volume-title":"Logic Colloquium","volume":"3","author":"Girard","year":"2003"},{"key":"S0960129520000250_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/11601548_23"},{"key":"S0960129520000250_ref23","unstructured":"Girard, J.-Y. (2013). Geometry of interaction VI: A blueprint for transcendental syntax. preprint."},{"key":"S0960129520000250_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_49"},{"key":"S0960129520000250_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129520000250_ref48","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"S0960129520000250_ref39","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"S0960129520000250_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"S0960129520000250_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"S0960129520000250_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.04.006"},{"key":"S0960129520000250_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.017"},{"key":"S0960129520000250_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)80713-4"},{"key":"S0960129520000250_ref8","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0960129520000250_ref10","unstructured":"Curien, P.-L. (2006). Notes on game semantics. From the author\u2019s web page."},{"key":"S0960129520000250_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47992-6"},{"key":"S0960129520000250_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983504"},{"key":"S0960129520000250_ref12","unstructured":"Danos, V. , Herbelin, H. and Regnier, L. (1996). Game semantics and abstract machines. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 394."},{"key":"S0960129520000250_ref24","volume-title":"Proofs and Types","volume":"7","author":"Girard","year":"1989"},{"key":"S0960129520000250_ref41","first-page":"39","volume-title":"Handbook of Logic in Computer Science","author":"Pitts","year":"2001"},{"key":"S0960129520000250_ref4","first-page":"1","volume-title":"Computational Logic","author":"Abramsky","year":"1999"},{"key":"S0960129520000250_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129520000250_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.011"},{"key":"S0960129520000250_ref31","volume-title":"Semantics and Logics of Computation","volume":"14","author":"Hyland","year":"1997"},{"key":"S0960129520000250_ref47","volume-title":"Lectures on the Curry-Howard Isomorphism","volume":"149","author":"S\u00f8rensen","year":"2006"},{"key":"S0960129520000250_ref42","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129520000250_ref5","first-page":"431","volume-title":"Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science","author":"Abramsky","year":"1999"},{"volume-title":"Handbook of Logic in Computer Science","year":"1994","author":"Abramsky","key":"S0960129520000250_ref3"},{"key":"S0960129520000250_ref33","volume-title":"Introduction to Higher-Order Categorical Logic","volume":"7","author":"Lambek","year":"1988"},{"key":"S0960129520000250_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.07.016"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129520000250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,19]],"date-time":"2024-08-19T13:38:59Z","timestamp":1724074739000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129520000250\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9]]},"references-count":48,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2020,9]]}},"alternative-id":["S0960129520000250"],"URL":"https:\/\/doi.org\/10.1017\/s0960129520000250","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2020,9]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}