{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:55Z","timestamp":1776316915162,"version":"3.50.1"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171261","type":"print"},{"value":"9783030171278","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present a framework for game semantics based on concurrent games, that keeps track of <jats:italic>resources<\/jats:italic> as data modified throughout execution but not affecting its control flow. Our leading example is <jats:italic>time<\/jats:italic>, yet the construction is in fact parametrized by a <jats:italic>resource bimonoid<\/jats:italic>\n            <jats:inline-formula>\n              <jats:tex-math>$$\\mathcal {R}$$<\/jats:tex-math>\n            <\/jats:inline-formula>, an algebraic structure expressing resources and the effect of their consumption either sequentially or in parallel. Relying on our construction, we give a sound resource-sensitive denotation to <jats:inline-formula>\n              <jats:tex-math>$$\\mathcal {R}$$<\/jats:tex-math>\n            <\/jats:inline-formula>-IPA, an affine higher-order concurrent programming language with shared state and a primitive for resource consumption in <jats:inline-formula>\n              <jats:tex-math>$$\\mathcal {R}$$<\/jats:tex-math>\n            <\/jats:inline-formula>. Compared with general operational semantics parametrized by <jats:inline-formula>\n              <jats:tex-math>$$\\mathcal {R}$$<\/jats:tex-math>\n            <\/jats:inline-formula>, our resource analysis turns out to be finer, leading to non-adequacy. Yet, our model is not degenerate as adequacy holds for an operational semantics specialized to time.<\/jats:p>\n          <jats:p>In regard to earlier semantic frameworks for tracking resources, the main novelty of our work is that it is based on a non-interleaving semantics, and as such accounts for <jats:italic>parallel<\/jats:italic> use of resources accurately.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_2","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"27-44","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Resource-Tracking Concurrent Games"],"prefix":"10.1007","author":[{"given":"Aurore","family":"Alcolei","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Clairambault","sequence":"additional","affiliation":[]},{"given":"Olivier","family":"Laurent","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1006\/inco.2000.2930","volume":"163","author":"S Abramsky","year":"2000","unstructured":"Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409\u2013470 (2000). https:\/\/doi.org\/10.1006\/inco.2000.2930","journal-title":"Inf. Comput."},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Abramsky, S., Melli\u00e8s, P.: Concurrent games and full completeness. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, 2\u20135 July 1999, pp. 431\u2013442 (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782638","DOI":"10.1109\/LICS.1999.782638"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Alcolei, A., Clairambault, P., Hyland, M., Winskel, G.: The true concurrency of Herbrand\u2019s theorem. In: 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, Birmingham, UK, 4\u20137 September 2018, pp. 5:1\u20135:22 (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2018.5","DOI":"10.4230\/LIPIcs.CSL.2018.5"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-54833-8_19","volume-title":"Programming Languages and Systems","author":"A Brunel","year":"2014","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 351\u2013370. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_19"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Castellan, S., Clairambault, P.: Causality vs. interleavings in concurrent game semantics. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, Qu\u00e9bec City, Canada, 23\u201326 August 2016. LIPIcs, vol. 59, pp. 32:1\u201332:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.32","DOI":"10.4230\/LIPIcs.CONCUR.2016.32"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Castellan, S., Clairambault, P., Paquet, H., Winskel, G.: The concurrent game semantics of probabilistic PCF. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09\u201312 July 2018, pp. 215\u2013224 (2018). https:\/\/doi.org\/10.1145\/3209108.3209187","DOI":"10.1145\/3209108.3209187"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Castellan, S., Clairambault, P., Rideau, S., Winskel, G.: Games and strategies as event structures. Logical Methods Comput. Sci. 13(3) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(3:35)2017","DOI":"10.23638\/LMCS-13(3:35)2017"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Castellan, S., Clairambault, P., Winskel, G.: The parallel intensionally fully abstract games model of PCF. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6\u201310 July 2015, pp. 232\u2013243 (2015). https:\/\/doi.org\/10.1109\/LICS.2015.31","DOI":"10.1109\/LICS.2015.31"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Castellan, S., Clairambault, P., Winskel, G.: Thin games with symmetry and concurrent hyland-ong games. Logical Methods Comput. Sci. (to appear, 2019)","DOI":"10.23638\/LMCS-15(1:18)2019"},{"issue":"POPL","key":"2_CR10","doi-asserted-by":"publisher","first-page":"32:1","DOI":"10.1145\/3290345","volume":"3","author":"P Clairambault","year":"2019","unstructured":"Clairambault, P., de Visme, M., Winskel, G.: Game semantics for quantum programming. PACMPL 3(POPL), 32:1\u201332:29 (2019). https:\/\/doi.org\/10.1145\/3290345","journal-title":"PACMPL"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.tcs.2011.11.027","volume":"424","author":"T Ehrhard","year":"2012","unstructured":"Ehrhard, T.: The Scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci. 424, 20\u201345 (2012). https:\/\/doi.org\/10.1016\/j.tcs.2011.11.027","journal-title":"Theor. Comput. Sci."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-02273-9_9","volume-title":"Typed Lambda Calculi and Applications","author":"C Faggian","year":"2009","unstructured":"Faggian, C., Piccolo, M.: Partial orders, event structures and linear strategies. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 95\u2013111. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02273-9_9"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Ghica, D.R.: Slot games: a quantitative model of computation. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, 12\u201314 January 2005, pp. 85\u201397 (2005). https:\/\/doi.org\/10.1145\/1040305.1040313","DOI":"10.1145\/1040305.1040313"},{"issue":"2\u20133","key":"2_CR14","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.apal.2007.10.005","volume":"151","author":"DR Ghica","year":"2008","unstructured":"Ghica, D.R., Murawski, A.S.: Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Logic 151(2\u20133), 89\u2013114 (2008). https:\/\/doi.org\/10.1016\/j.apal.2007.10.005","journal-title":"Ann. Pure Appl. Logic"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-54833-8_18","volume-title":"Programming Languages and Systems","author":"DR Ghica","year":"2014","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 331\u2013350. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18"},{"issue":"6","key":"2_CR16","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/j.jlap.2011.04.005","volume":"80","author":"T Hoare","year":"2011","unstructured":"Hoare, T., M\u00f6ller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266\u2013296 (2011). https:\/\/doi.org\/10.1016\/j.jlap.2011.04.005","journal-title":"J. Log. Algebr. Program."},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"JME Hyland","year":"2000","unstructured":"Hyland, J.M.E., Ong, C.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285\u2013408 (2000). https:\/\/doi.org\/10.1006\/inco.2000.2917","journal-title":"Inf. Comput."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Laird, J., Manzonetto, G., McCusker, G., Pagani, M.: Weighted relational models of typed lambda-calculi. In: 28th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), New Orleans, USA, Proceedings, pp. 301\u2013310 (2013)","DOI":"10.1109\/LICS.2013.36"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Laurent, O.: Game semantics for first-order logic. Logical Methods Comput. Sci. 6(4) (2010). https:\/\/doi.org\/10.2168\/LMCS-6(4:3)2010","DOI":"10.2168\/LMCS-6(4:3)2010"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Melli\u00e8s, P.: Asynchronous games 4: a fully complete model of propositional linear logic. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, 26\u201329 June 2005, Proceedings, pp. 386\u2013395 (2005). https:\/\/doi.org\/10.1109\/LICS.2005.6","DOI":"10.1109\/LICS.2005.6"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Melli\u00e8s, P.: Game semantics in string diagrams. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, 25\u201328 June 2012, pp. 481\u2013490 (2012). https:\/\/doi.org\/10.1109\/LICS.2012.58","DOI":"10.1109\/LICS.2012.58"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-540-74407-8_27","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"P-A Melli\u00e8s","year":"2007","unstructured":"Melli\u00e8s, P.-A., Mimram, S.: Asynchronous games: innocence without alternation. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 395\u2013411. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_27"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Mittermayr, R., Blieberger, J.: Timing analysis of concurrent programs. In: Vardanega, T. (ed.) 12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, Pisa, Italy, 10 July 2012. OASICS, vol. 23, pp. 59\u201368. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012). https:\/\/doi.org\/10.4230\/OASIcs.WCET.2012.59","DOI":"10.4230\/OASIcs.WCET.2012.59"},{"key":"2_CR24","unstructured":"Plotkin, G.D.: Post-graduate lecture notes in advanced domain theory (incorporating the \u201cPisa notes\u201d). Department of Computer Science, University of Edinburgh (1981)"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Rideau, S., Winskel, G.: Concurrent strategies. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, Toronto, Ontario, Canada, 21\u201324 June 2011, pp. 409\u2013418 (2011). https:\/\/doi.org\/10.1109\/LICS.2011.13","DOI":"10.1109\/LICS.2011.13"},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-1-4471-3196-0_24","volume-title":"Functional Programming, Glasgow 1991","author":"D Sands","year":"1991","unstructured":"Sands, D.: Operational theories of improvement in functional languages (extended abstract). In: Heldal, R., Holst, C.K., Wadler, P. (eds.) Functional Programming, Glasgow 1991, pp. 298\u2013311. Springer, London (1991). https:\/\/doi.org\/10.1007\/978-1-4471-3196-0_24"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"G Winskel","year":"1987","unstructured":"Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325\u2013392. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-17906-2_31"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17127-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T22:22:59Z","timestamp":1753309379000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}