{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T17:06:43Z","timestamp":1776272803654,"version":"3.50.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227294","type":"print"},{"value":"9783032227300","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22730-0_18","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T16:24:24Z","timestamp":1776270264000},"page":"372-395","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Interaction Improvement"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-5481-5719","authenticated-orcid":false,"given":"Adrienne","family":"Lancelot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1448-9014","authenticated-orcid":false,"given":"Giulio","family":"Manzonetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0305-6398","authenticated-orcid":false,"given":"Guy","family":"McCusker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-8674","authenticated-orcid":false,"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","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","DOI":"10.1006\/INCO.2000.2930"},{"issue":"2","key":"18_CR2","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1006\/INCO.1993.1044","volume":"105","author":"S Abramsky","year":"1993","unstructured":"Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159\u2013267 (1993). https:\/\/doi.org\/10.1006\/INCO.1993.1044","journal-title":"Inf. Comput."},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Dal\u00a0Lago, U., Vanoni, G.: Multi types and reasonable space. Proc. ACM Program. Lang. 6(ICFP), 799\u2013825 (2022). https:\/\/doi.org\/10.1145\/3547650","DOI":"10.1145\/3547650"},{"key":"18_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X","volume":"30","author":"B Accattoli","year":"2020","unstructured":"Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds, fully developed. J. Funct. Program. 30, e14 (2020). https:\/\/doi.org\/10.1017\/S095679682000012X","journal-title":"J. Funct. Program."},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Lancelot, A., Manzonetto, G., Vanoni, G.: Interaction equivalence. Proc. ACM Program. Lang. 9(POPL) (Jan 2025). https:\/\/doi.org\/10.1145\/3704891, https:\/\/doi.org\/10.1145\/3704891","DOI":"10.1145\/3704891"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Alcolei, A., Clairambault, P., Laurent, O.: Resource-tracking concurrent games. In: Bojanczyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11425, pp. 27\u201344. Springer (2019).https:\/\/doi.org\/10.1007\/978-3-030-17127-8_2","DOI":"10.1007\/978-3-030-17127-8_2"},{"key":"18_CR7","unstructured":"Barendregt, H.: The Lambda Calculus \u2013 Its Syntax and Semantics, Studies in logic and the foundations of mathematics, vol.\u00a0103. North-Holland (1984)"},{"key":"18_CR8","unstructured":"Berry, G.: Some syntactic and categorical constructions of lambda-calculus models. Research Report RR-0080, INRIA (1981), https:\/\/inria.hal.science\/inria-00076481"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normal-form bisimilarity for state. In: Bojanczyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11425, pp. 98\u2013114. Springer (2019https:\/\/doi.org\/10.1007\/978-3-030-17127-8_6, https:\/\/doi.org\/10.1007\/978-3-030-17127-8_6","DOI":"10.1007\/978-3-030-17127-8_6"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Biernacki, D., Lenglet, S., Polesiuk, P.: A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0167, pp. 7:1\u20137:22. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.7, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/12329","DOI":"10.4230\/LIPIcs.FSCD.2020.7"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Biernacki, D., Lenglet, S., Polesiuk, P.: Proving soundness of extensional normal-form bisimilarities. Electronic Notes in Theoretical Computer Science 336, 41\u201356 (2018). https:\/\/doi.org\/10.1016\/j.entcs.2018.03.015, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066118300185, the Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII)","DOI":"10.1016\/j.entcs.2018.03.015"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Breuvart, F., Manzonetto, G., Ruoppolo, D.: Relational graph models at work. Log. Methods Comput. Sci. 14(3) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(3:2)2018, https:\/\/doi.org\/10.23638\/LMCS-14(3:2)2018","DOI":"10.23638\/LMCS-14(3:2)2018"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Not enough points is enough. In: Duparc, J., Henzinger, T.A. (eds.) Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04646, pp. 298\u2013312. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_24, https:\/\/doi.org\/10.1007\/978-3-540-74915-8_24","DOI":"10.1007\/978-3-540-74915-8_24"},{"issue":"4","key":"18_CR14","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1093\/JIGPAL\/JZX018","volume":"25","author":"A Bucciarelli","year":"2017","unstructured":"Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL 25(4), 431\u2013464 (2017). https:\/\/doi.org\/10.1093\/JIGPAL\/JZX018","journal-title":"Log. J. IGPL"},{"key":"18_CR15","unstructured":"de Carvalho, D.: S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille II (2007)"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"de Carvalho, D.: Execution time of $$\\lambda $$-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci. 28(7), 1169\u20131203 (2018). https:\/\/doi.org\/10.1017\/S0960129516000396","DOI":"10.1017\/S0960129516000396"},{"key":"18_CR17","unstructured":"Clairambault, P.: Causal Investigations in Interactive Semantics. Habilitation \u00e0 diriger des recherches, Aix-Marseille Universit\u00e9, Marseille, France (2024), https:\/\/tel.archives-ouvertes.fr\/tel-04523273"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Dal\u00a0Lago, U., Gavazzo, F.: Effectful Normal Form Bisimulation. In: ESOP 2019 - European Symposium on Programming. Prague, Czech Republic (Apr 2019), https:\/\/hal.inria.fr\/hal-02386004","DOI":"10.1007\/978-3-030-17184-1_10"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Ehrhard, T., Pagani, M., Tasson, C.: Full abstraction for probabilistic PCF. J. ACM 65(4), 23:1\u201323:44 (2018). https:\/\/doi.org\/10.1145\/3164540, https:\/\/doi.org\/10.1145\/3164540","DOI":"10.1145\/3164540"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Fokkink, W.J.: Modelling Distributed Systems. Springer, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-49321-0","DOI":"10.1007\/978-3-540-49321-0"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Ghica, D.R.: Slot games: a quantitative model of computation. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. pp. 85\u201397. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040313","DOI":"10.1145\/1040305.1040313"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103\u2013112 (1996). https:\/\/doi.org\/10.1006\/inco.1996.0008, https:\/\/doi.org\/10.1006\/inco.1996.0008","DOI":"10.1006\/inco.1996.0008"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Hyland, M.: A syntactic characterization of the equality in some models for the lambda calculus. Journal of the London Mathematical Society s2-12(3), 361\u2013370 (1976). https:\/\/doi.org\/10.1112\/jlms\/s2-12.3.361","DOI":"10.1112\/jlms\/s2-12.3.361"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Hyland, M., Nagayama, M., Power, J., Rosolini, G.: A category theoretic formulation for engeler-style models of the untyped lambda. In: Seda, A.K., Hurley, T., Schellekens, M.P., an\u00a0Airchinnigh, M.M., Strong, G. (eds.) Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2004, Dublin, Ireland, July 22-23, 2004. Electronic Notes in Theoretical Computer Science, vol.\u00a0161, pp. 43\u201357. Elsevier (2004). https:\/\/doi.org\/10.1016\/J.ENTCS.2006.04.024, https:\/\/doi.org\/10.1016\/j.entcs.2006.04.024","DOI":"10.1016\/J.ENTCS.2006.04.024"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Hyland, M., 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","DOI":"10.1006\/INCO.2000.2917"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Ker, A.D., Nickau, H., Ong, C.L.: Innocent game models of untyped lambda-calculus. Theor. Comput. Sci. 272(1\u20132), 247\u2013292 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(00)00353-4, https:\/\/doi.org\/10.1016\/S0304-3975(00)00353-4","DOI":"10.1016\/S0304-3975(00)00353-4"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Ker, A.D., Nickau, H., Ong, C.L.: Adapting innocent game models for the b\u00f6hm tree $$\\lambda $$-theory. Theor. Comput. Sci. 308(1\u20133), 333\u2013366 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(02)00849-6","DOI":"10.1016\/S0304-3975(02)00849-6"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Koutavas, V., Lin, Y.Y., Tzevelekos, N.: Fully abstract normal form bisimulation for call-by-value pcf. In: 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201313 (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175778","DOI":"10.1109\/LICS56636.2023.10175778"},{"key":"18_CR29","doi-asserted-by":"publisher","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 2013, New Orleans, LA, USA, June 25-28, 2013. pp. 301\u2013310. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/LICS.2013.36, https:\/\/doi.org\/10.1109\/LICS.2013.36","DOI":"10.1109\/LICS.2013.36"},{"key":"18_CR30","unstructured":"Lancelot, A., Manzonetto, G., McCusker, G., Vanoni, G.: Interaction improvement (2026), https:\/\/arxiv.org\/abs\/2601.01638"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Lassen, S.B.: Bisimulation in untyped lambda calculus: B\u00f6hm trees and bisimulation up to context. Electronic Notes in Theoretical Computer Science 20, 346\u2013374 (1999). https:\/\/doi.org\/10.1016\/S1571-0661(04)80083-5","DOI":"10.1016\/S1571-0661(04)80083-5"},{"key":"18_CR32","doi-asserted-by":"publisher","unstructured":"Levy, P.B., Staton, S.: Transition systems over games. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS \u201914, Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2603088.2603150, https:\/\/doi.org\/10.1145\/2603088.2603150","DOI":"10.1145\/2603088.2603150"},{"key":"18_CR33","unstructured":"Morris, J.H.: Lambda-calculus Models of Programming Languages. Ph.D. thesis, Massachusetts Institute of Technology (1968), https:\/\/books.google.is\/books?id=DklAAQAAIAAJ"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Paolini, L., Piccolo, M., Ronchi Della\u00a0Rocca, S.: Essential and relational models. Math. Struct. Comput. Sci. 27(5), 626\u2013650 (2017). https:\/\/doi.org\/10.1017\/S0960129515000316, https:\/\/doi.org\/10.1017\/S0960129515000316","DOI":"10.1017\/S0960129515000316"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Patrignani, M., Ahmed, A., Clarke, D.: Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput. Surv. 51(6), 125:1\u2013125:36 (2019). https:\/\/doi.org\/10.1145\/3280984","DOI":"10.1145\/3280984"},{"key":"18_CR36","doi-asserted-by":"publisher","unstructured":"Pitts, A.M.: Howe\u2019s method for higher-order languages. In: Sangiorgi, D., Rutten, J.J.M.M. (eds.) Advanced Topics in Bisimulation and Coinduction, Cambridge tracts in theoretical computer science, vol.\u00a052, pp. 197\u2013232. Cambridge University Press (2012). https:\/\/doi.org\/10.1017\/CBO9780511792588.006","DOI":"10.1017\/CBO9780511792588.006"},{"key":"18_CR37","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D.: A powerdomain construction. SIAM J. Comput. 5(3), 452\u2013487 (1976). https:\/\/doi.org\/10.1137\/0205035, https:\/\/doi.org\/10.1137\/0205035","DOI":"10.1137\/0205035"},{"key":"18_CR38","doi-asserted-by":"publisher","unstructured":"Ronchi Della\u00a0Rocca, S.: Characterization theorems for a filter lambda model. Inf. Control. 54(3), 201\u2013216 (1982). https:\/\/doi.org\/10.1016\/S0019-9958(82)80022-3, https:\/\/doi.org\/10.1016\/S0019-9958(82)80022-3","DOI":"10.1016\/S0019-9958(82)80022-3"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Sands, D.: Proving the correctness of recursion-based automatic program transformations. Theor. Comput. Sci. 167(1&2), 193\u2013233 (1996). https:\/\/doi.org\/10.1016\/0304-3975(96)00074-6","DOI":"10.1016\/0304-3975(96)00074-6"},{"key":"18_CR40","doi-asserted-by":"publisher","unstructured":"Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Trans. Program. Lang. Syst. 18(2), 175\u2013234 (mar 1996). https:\/\/doi.org\/10.1145\/227699.227716","DOI":"10.1145\/227699.227716"},{"key":"18_CR41","unstructured":"Sands, D.: Improvement theory and its applications, p. 275\u2013306. Cambridge University Press, USA (1999)"},{"key":"18_CR42","unstructured":"Scott, D., Strachey, C.: Toward a mathematical semantics for computer languages. In: MRI Symposium Proceedings, vol. 21: Proceedings of the Symposium on Computers and Automata. pp. 19\u201346. Fox, J. (Ed.). Polytechnic Press, Polytechnic Institute of Brooklyn, New York (1971)"},{"key":"18_CR43","doi-asserted-by":"crossref","unstructured":"St\u00f8vring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequential control and state. In: Proc. 34th Annual ACM Symposium on Principles of Programming Languages. pp. 161\u2013172. Nice, France (2007), http:\/\/doi.acm.org\/10.1145\/1190215.1190244","DOI":"10.1145\/1190216.1190244"},{"issue":"3","key":"18_CR44","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1137\/0205036","volume":"5","author":"CP Wadsworth","year":"1976","unstructured":"Wadsworth, C.P.: The Relation Between Computational and Denotational Properties for Scott\u2019s $$\\cal{D} _\\infty $$-Models of the Lambda-Calculus. SIAM J. Comput. 5(3), 488\u2013521 (1976). https:\/\/doi.org\/10.1137\/0205036","journal-title":"SIAM J. Comput."}],"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-032-22730-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T16:24:26Z","timestamp":1776270266000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22730-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227294","9783032227300"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22730-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","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":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2026\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}