{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:47:43Z","timestamp":1775868463755,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>Game semantics and session types are two formalisations of the same concept: message-passing open programs following certain protocols. Game semantics represents protocols as games, and programs as strategies; while session types specify protocols, and well-typed \u03c0-calculus processes model programs. Giving faithful models of the \u03c0-calculus and giving a precise description of strategies as a programming language are two difficult problems. In this paper, we show how these two problems can be tackled at the same time by building an accurate game semantics model of the session \u03c0-calculus.<\/jats:p>\n          <jats:p>Our main contribution is to fill a semantic gap between the synchrony of the (session) \u03c0-calculus and the asynchrony of game semantics, by developing an event-structure based game semantics for synchronous concurrent computation. This model supports the first truly concurrent fully abstract (for barbed congruence) interpretation of the synchronous (session) \u03c0-calculus. We further strengthen this correspondence, establishing finite definability of asynchronous strategies by the internal session \u03c0-calculus. As an application of these results, we propose a faithful encoding of synchronous strategies into asynchronous strategies by call-return protocols, which induces automatically an encoding at the level of processes. Our results bring session types and game semantics into the same picture, proposing the session calculus as a programming language for strategies, and strategies as a very accurate model of the session calculus. We implement a prototype which computes the interpretation of session processes as synchronous strategies.<\/jats:p>","DOI":"10.1145\/3290340","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side"],"prefix":"10.1145","volume":"3","author":[{"given":"Simon","family":"Castellan","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_2_2_2_1","volume-title":"A Fully Abstract Game Semantics for General References (LICS\u201998)","author":"Abramsky Samson"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/645868.668491"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00047-X"},{"key":"e_1_2_2_6_1","volume-title":"Concurrent Games and Full Completeness. In 14th Annual IEEE Symposium on Logic in Computer Science","author":"Abramsky Samson","year":"1999"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_3"},{"key":"e_1_2_2_8_1","volume-title":"Proceedings of the 26th International Conference on Concurrency Theory (CONCUR\u201915) (Leibniz International Proceedings in Informatics), Luca Aceto and David de Frutos-Escrig (Eds.)","volume":"42","author":"Baelde David","year":"2015"},{"key":"e_1_2_2_9_1","volume-title":"Typed Lambda Calculi and Applications (Lecture Notes in Computer Science)","author":"Berger Martin"},{"key":"e_1_2_2_10_1","volume-title":"FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 3\u201319","author":"Castellan Simon","year":"2018"},{"key":"e_1_2_2_11_1","volume-title":"Games and Strategies as Event Structures. Logical Methods in Computer Science","author":"Castellan Simon","year":"2017"},{"key":"e_1_2_2_12_1","unstructured":"Simon Castellan and Nobuko Yoshida. 2018. Two sides of the same coin: Session Types and Game Semantics. (2018). https:\/\/www.doc.ic.ac.uk\/research\/technicalreports\/2018\/DTRS18- 5.pdf Technical report.  Simon Castellan and Nobuko Yoshida. 2018. Two sides of the same coin: Session Types and Game Semantics. (2018). https:\/\/www.doc.ic.ac.uk\/research\/technicalreports\/2018\/DTRS18- 5.pdf Technical report."},{"key":"e_1_2_2_13_1","volume-title":"Presheaf models for concurrency","author":"Cattani Gian Luca"},{"key":"e_1_2_2_14_1","first-page":"1","article-title":"On the Preciseness of Subtyping in Session Types","volume":"13","author":"Chen Tzu-Chun","year":"2017","journal-title":"LMCS"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392224"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_14"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/507382.507385"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.20"},{"key":"e_1_2_2_19_1","volume-title":"Fully-abstract concurrent games for pi. CoRR abs\/1310.4306","author":"Eberhart Clovis","year":"2013"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2697442.2697675"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_2_22_1","volume-title":"Menaa","author":"Ghica Dan R.","year":"2011"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788970"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Matthew Hennessy. 2007. A Distributed Pi-Calculus. CUP.   Matthew Hennessy. 2007. A Distributed Pi-Calculus. CUP.","DOI":"10.1017\/CBO9780511611063"},{"key":"e_1_2_2_25_1","volume-title":"ECOOP\u201991 (LNCS)","author":"Honda Kohei"},{"key":"e_1_2_2_26_1","volume-title":"ESOP (LNCS)","author":"Honda Kohei"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00074-7"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00039-0"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224189"},{"key":"e_1_2_2_33_1","volume-title":"Globally Governed Session Semantics. LMCS 10","author":"Kouzapas Dimitrios","year":"2015"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788859"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80965-4"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_8"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.6"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.016"},{"key":"e_1_2_2_39_1","unstructured":"Paul-Andr\u00e9 Melli\u00e8s. 2019. Categorical combinatorics of scheduling and synchronization for games and strategies. In Accepted for publication at POPL\u201919.  Paul-Andr\u00e9 Melli\u00e8s. 2019. Categorical combinatorics of scheduling and synchronization for games and strategies. In Accepted for publication at POPL\u201919."},{"key":"e_1_2_2_40_1","volume-title":"Asynchronous Games: Innocence Without Alternation. In CONCUR 2007 -Concurrency Theory, 18th International Conference. 395\u2013411","author":"Melli\u00e8s Paul-Andr\u00e9","year":"2007"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209116"},{"key":"e_1_2_2_42_1","first-page":"119","article-title":"Functions as Processes","volume":"2","author":"Milner Robin","year":"1992","journal-title":"MSCS"},{"key":"e_1_2_2_43_1","volume-title":"ICALP (LNCS)","author":"Milner Robin"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/2779624.2779717"},{"key":"e_1_2_2_45_1","volume-title":"Seminar on Concurrency","author":"Pratt Vaughan R.","year":"1984"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.13"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_23"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/646249.685350"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/646732.701294"},{"key":"e_1_2_2_51_1","volume-title":"PARLE\u201994 (LNCS)","author":"Takeuchi Kaku"},{"key":"e_1_2_2_52_1","volume-title":"March 14, 2002}. 244\u2013256","author":"Thiagarajan P. S.","year":"2002"},{"key":"e_1_2_2_53_1","volume-title":"Bundle Event Structures and CCSP. In CONCUR 2003 - Concurrency Theory, Roberto Amadio and Denis Lugiez (Eds.). Springer Berlin Heidelberg","author":"van Glabbeek Rob","year":"2003"},{"key":"e_1_2_2_55_1","volume-title":"Proceedings of an Advanced Course, Bad Honnef, 8.-19","author":"Winskel Glynn","year":"1986"},{"key":"e_1_2_2_56_1","volume-title":"FSTTCS (LNCS)","author":"Yoshida Nobuko"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290340"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290340"],"URL":"https:\/\/doi.org\/10.1145\/3290340","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}