{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T13:44:54Z","timestamp":1748439894880,"version":"3.40.3"},"publisher-location":"Cham","reference-count":75,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572616"},{"type":"electronic","value":"9783031572623"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We build on a fine-grained analysis of session-based interaction as provided by the linear logic typing disciplines to introduce the SAM, an abstract machine for mechanically executing session-typed processes. A remarkable feature of the SAM\u2019s design is its ability to naturally segregate and coordinate sequential with concurrent session behaviours. In particular, implicitly sequential parts of session programs may be efficiently executed by deterministic sequential application of SAM transitions, amenable to compilation, and without concurrent synchronisation mechanisms. We provide an intuitive discussion of the SAM structure and its underlying design, and state and prove its correctness for executing programs in a session calculus corresponding to full classical linear logic<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{CLL}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>CLL<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. We also discuss extensions and applications of the SAM to the execution of linear and session-based programming languages.<\/jats:p>","DOI":"10.1007\/978-3-031-57262-3_9","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"206-235","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The Session Abstract Machine"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Caires","sequence":"first","affiliation":[]},{"given":"Bernardo","family":"Toninho","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Computational Interpretations of Linear Logic. Theoret. Comput. Sci. 111(1\u20132), 3\u201357 (1993)","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Gay, S.J., Nagarajan, R.: Interaction categories and the foundations of typed concurrent programming. In: NATO ASI DPD. pp. 35\u2013113 (1996)","DOI":"10.1007\/978-3-642-61455-2_10"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, B., Mordido, A., Thiemann, P., Vasconcelos, V.T.: Polymorphic lambda calculus with context-free session types. Inf. Comput. 289(Part), 104948 (2022)","DOI":"10.1016\/j.ic.2022.104948"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Andreoli, J.M.: Logic Programming with Focusing Proofs in Linear Logic. J. Log. Comput. 2(3), 297\u2013347 (1992)","DOI":"10.1093\/logcom\/2.3.297"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Balzer, S., Pfenning, F.: Manifest sharing with session types. Proc. ACM Program. Lang. 1(ICFP) (2017)","DOI":"10.1145\/3110281"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Bellin, G., Scott, P.: On the $$\\pi $$-calculus and linear logic. Theoret. Comput. Sci. 135(1), 11\u201365 (1994)","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models. In: International Workshop on Computer Science Logic. pp. 121\u2013135. Springer (1994)","DOI":"10.1007\/BFb0022251"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Bernardy, J., Boespflug, M., Newton, R.R., Jones, S.P., Spiwack, A.: Linear haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2(POPL), 5:1\u20135:29 (2018)","DOI":"10.1145\/3158093"},{"key":"9_CR9","unstructured":"Blackshear, S., Cheng, E., Dill, D.L., Gao, V., Maurer, B., Nowacki, T., Pott, A., Qadeer, S., Russi, D., Sezer, D., Zakian, T., Zhou, R.: Move: A Language with Programmable Resources (2019)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Caires, L., P\u00e9rez, J.A.: Linearity, control effects, and behavioral types. In: Yang, H. (ed.) Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017. Lecture Notes in Computer Science, vol. 10201, pp. 229\u2013259. Springer (2017)","DOI":"10.1007\/978-3-662-54434-1_9"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Caires, L., P\u00e9rez, J.A.: Linearity, control effects, and behavioral types. In: Proceedings of the 26th European Symposium on Programming Languages and Systems - Volume 10201. p. 229\u2013259. Springer-Verlag, Berlin, Heidelberg (2017)","DOI":"10.1007\/978-3-662-54434-1_9"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Caires, L., P\u00e9rez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Proceedings of the 22nd European Conference on Programming Languages and Systems. p. 330\u2013349. ESOP\u201913, Springer-Verlag, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory. pp. 222\u2013236. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Caires, L., Pfenning, F., Toninho, B.: Towards concurrent type theory. In: Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation. p. 1\u201312. TLDI \u201912, Association for Computing Machinery, New York, NY, USA (2012)","DOI":"10.1145\/2103786.2103788"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Mathematical Structures in Computer Science 26(3), 367\u2013423 (2016)","DOI":"10.1017\/S0960129514000218"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Caires, L., Toninho, B.: The session abstract machine (extended version) (2024)","DOI":"10.1007\/978-3-031-57262-3_9"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Caires, L., Toninho, B.: The Session Abstract Machine (Artifact) (2024). https:\/\/doi.org\/10.5281\/zenodo.10459455","DOI":"10.5281\/zenodo.10459455"},{"key":"9_CR18","unstructured":"Cardelli, L.: Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts pp. 431\u2013507 (1991)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Castellan, S., Yoshida, N.: Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side. Proc. ACM Program. Lang. 3(POPL), 27:1\u201327:29 (2019)","DOI":"10.1145\/3290340"},{"key":"9_CR20","unstructured":"Chen, R., Balzer, S., Toninho, B.: Ferrite: A Judgmental Embedding of Session Types in Rust. In: Ali, K., Vitek, J. (eds.) 36th European Conference on Object-Oriented Programming, ECOOP 2022. LIPIcs, vol.\u00a0222, pp. 22:1\u201322:28 (2022)"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Cousineau, G., Curien, P., Mauny, M.: The Categorical Abstract Machine. Sci. Comput. Program. 8(2), 173\u2013202 (1987)","DOI":"10.1016\/0167-6423(87)90020-7"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Danvy, O.: A Rational Deconstruction of Landin\u2019s SECD Machine. In: Grelck, C., Huch, F., Michaelson, G., Trinder, P.W. (eds.) Implementation and Application of Functional Languages, 16th International Workshop, IFL 2004. LNCS, vol.\u00a03474, pp. 52\u201371. Springer (2004)","DOI":"10.1007\/11431664_4"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session-typed processes. In: Baier, C., Lago, U.D. (eds.) Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018. LNCS, vol. 10803, pp. 91\u2013109. Springer (2018)","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Das, A., Pfenning, F.: Rast: A language for resource-aware session types. Log. Methods Comput. Sci. 18(1) (2022)","DOI":"10.46298\/lmcs-18(1:9)2022"},{"key":"9_CR25","unstructured":"DeYoung, H., Caires, L., Pfenning, F., Toninho, B.: Cut reduction in linear logic as asynchronous session-typed communication. In: Computer Science Logic (2012)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Franco, J., Vasconcelos, V.T.: A concurrent programming language with refined session types. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) Software Engineering and Formal Methods - SEFM 2013. LNCS, vol.\u00a08368, pp. 15\u201328. Springer (2013)","DOI":"10.1007\/978-3-319-05032-4_2"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Frumin, D., D\u2019Osualdo, E., van\u00a0den Heuvel, B., P\u00e9rez, J.A.: A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency. Proc. ACM Program. Lang. 6(OOPSLA2), 841\u2013869 (2022)","DOI":"10.1145\/3563318"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Gay, S., Hole, M.: Subtyping for Session Types in the Pi Calculus. Acta Informatica 42(2-3), 191\u2013225 (2005)","DOI":"10.1007\/s00236-005-0177-z"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Gay, S., Vasconcelos, V.: Linear Type Theory for Asynchronous Session Types. Journal of Functional Programming 20(1), 19\u201350 (2010)","DOI":"10.1017\/S0956796809990268"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Girard, J.: A new constructive logic: Classical logic. Math. Struct. Comput. Sci. 1(3), 255\u2013296 (1991)","DOI":"10.1017\/S0960129500001328"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR\u201993. pp. 509\u2013523. Springer Berlin Heidelberg, Berlin, Heidelberg (1993)","DOI":"10.1007\/3-540-57208-2_35"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Honda, K., Laurent, O.: An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci. 411(22-24), 2223\u20132238 (2010)","DOI":"10.1016\/j.tcs.2010.01.028"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) Programming Languages and Systems. pp. 122\u2013138. Springer (1998)","DOI":"10.1007\/BFb0053567"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., et\u00a0al.: Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49(1), \u00a03 (2016)","DOI":"10.1145\/2873052"},{"key":"9_CR35","unstructured":"Imai, K., Neykova, R., Yoshida, N., Yuen, S.: Multiparty session programming with global protocol combinators. In: Hirschfeld, R., Pape, T. (eds.) 34th European Conference on Object-Oriented Programming, ECOOP 2020. LIPIcs, vol.\u00a0166, pp. 9:1\u20139:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Jacobs, J., Balzer, S.: Higher-order leak and deadlock free locks. Proc. ACM Program. Lang. 7(POPL), 1027\u20131057 (2023)","DOI":"10.1145\/3571229"},{"key":"9_CR37","unstructured":"Klabnik, S., Nichols, C.: The Rust Programming Language (2021)"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Kokke, W., Dardha, O.: Deadlock-free session types in linear Haskell. In: Hage, J. (ed.) Haskell 2021: Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell. pp. 1\u201313. ACM (2021)","DOI":"10.1145\/3471874.3472979"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Kokke, W., Montesi, F., Peressotti, M.: Better late than never: a fully-abstract semantics for classical processes. Proc. ACM Program. Lang. 3(POPL), 24:1\u201324:29 (2019)","DOI":"10.1145\/3290337"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Krivine, J.: A call-by-name Lambda-calculus Machine. High. Order Symb. Comput. 20(3), 199\u2013207 (2007)","DOI":"10.1007\/s10990-007-9018-9"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Lafont, Y.: The Linear Abstract Machine. Theor. Comput. Sci. 59, 157\u2013180 (1988)","DOI":"10.1016\/0304-3975(88)90100-4"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"Lagaillardie, N., Neykova, R., Yoshida, N.: Implementing Multiparty Session Types in Rust. In: Coordination Models and Languages Coordination 2020. Lecture Notes in Computer Science, vol. 12134, pp. 127\u2013136. Springer (2020)","DOI":"10.1007\/978-3-030-50029-0_8"},{"key":"9_CR43","doi-asserted-by":"crossref","unstructured":"Landin, P.J.: The Mechanical Evaluation of Expressions. The Computer Journal, Volume 6, Issue 4, January 1964 6(4), 308\u2013320 (1964)","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"Laurent, O.: Polarized Proof-Nets: Proof-Nets for LC. In: Girard, J. (ed.) Typed Lambda Calculi and Applications, 4th International Conference, TLCA\u201999. LNCS, vol.\u00a01581, pp. 213\u2013227. Springer (1999)","DOI":"10.1007\/3-540-48959-2_16"},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"Lindley, S., Morris, J.G.: Embedding session types in Haskell. In: Mainland, G. (ed.) Proceedings of the 9th International Symposium on Haskell, Haskell 2016, Nara, Japan, September 22-23, 2016. pp. 133\u2013145. ACM (2016)","DOI":"10.1145\/2976002.2976018"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"Lopes, L.M.B., Silva, F.M.A., Vasconcelos, V.T.: A virtual machine for a process calculus. In: Nadathur, G. (ed.) Principles and Practice of Declarative Programming, International Conference PPDP\u201999. Lecture Notes in Computer Science, vol.\u00a01702, pp. 244\u2013260. Springer (1999)","DOI":"10.1007\/10704567_15"},{"key":"9_CR47","doi-asserted-by":"crossref","unstructured":"Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119\u2013141 (1992)","DOI":"10.1017\/S0960129500001407"},{"key":"9_CR48","doi-asserted-by":"crossref","unstructured":"Milner, R.: Elements of interaction: Turing award lecture. Communications of the ACM 36(1), 78\u201389 (1993)","DOI":"10.1145\/151233.151240"},{"key":"9_CR49","unstructured":"Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)"},{"key":"9_CR50","doi-asserted-by":"crossref","unstructured":"Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Gr\u00e4del, E., Kahle, R. (eds.) Computer Science Logic, 23rd international Workshop, CSL 2009. LNCS, vol.\u00a05771, pp. 409\u2013423. Springer (2009)","DOI":"10.1007\/978-3-642-04027-6_30"},{"key":"9_CR51","doi-asserted-by":"crossref","unstructured":"Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in f#. In: Dubach, C., Xue, J. (eds.) Proceedings of the 27th International Conference on Compiler Construction, CC 2018, February 24-25, 2018, Vienna, Austria. pp. 128\u2013138. ACM (2018)","DOI":"10.1145\/3178372.3179495"},{"key":"9_CR52","doi-asserted-by":"crossref","unstructured":"Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017)","DOI":"10.1017\/S0956796816000289"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"P\u00e9rez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations and observational equivalences for session-based concurrency. Information and Computation 239, 254\u2013302 (2014)","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"9_CR54","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Pruiksma, K.: Relating message passing and shared memory, proof-theoretically. In: Jongmans, S., Lopes, A. (eds.) Coordination Models and Languages - COORDINATION 2023. LNCS, vol. 13908, pp. 3\u201327. Springer (2023)","DOI":"10.1007\/978-3-031-35361-1_1"},{"key":"9_CR55","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Structural cut elimination. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science. p.\u00a0156. LICS \u201995, IEEE Computer Society, USA (1995)","DOI":"10.1109\/LICS.1995.523253"},{"key":"9_CR56","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Griffith, D.: Polarized Substructural Session Types. In: Proc. of FoSSaCS 2015. LNCS, vol.\u00a09034, pp. 3\u201322. Springer (2015)","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"9_CR57","doi-asserted-by":"crossref","unstructured":"Pierce, B.C., Turner, D.N.: Pict: a programming language based on the pi-calculus. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner. pp. 455\u2013494. The MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0022"},{"key":"9_CR58","doi-asserted-by":"crossref","unstructured":"Po\u00e7as, D., Costa, D., Mordido, A., Vasconcelos, V.T.: System f$$^{\\mu }$$ \u00f8mega with context-free session types. In: Wies, T. (ed.) Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023. LNCS, vol. 13990, pp. 392\u2013420. Springer (2023)","DOI":"10.1007\/978-3-031-30044-8_15"},{"key":"9_CR59","doi-asserted-by":"crossref","unstructured":"Qian, Z., Kavvos, G., Birkedal, L.: Client-server sessions in linear logic. Proceedings of the ACM on Programming Languages 5(ICFP), 1\u201331 (2021)","DOI":"10.1145\/3473567"},{"key":"9_CR60","doi-asserted-by":"crossref","unstructured":"Rocha, P., Caires, L.: Propositions-as-types and Shared State. Proceedings of the ACM on Programming Languages 5(ICFP), 1\u201330 (2021)","DOI":"10.1145\/3473584"},{"key":"9_CR61","doi-asserted-by":"crossref","unstructured":"Rocha, P., Caires, L.: Safe session-based concurrency with shared linear state. In: Wies, T. (ed.) Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023. LNCS, vol. 13990, pp. 421\u2013450. Springer (2023)","DOI":"10.1007\/978-3-031-30044-8_16"},{"key":"9_CR62","doi-asserted-by":"publisher","unstructured":"Rocha, P., Caires, L.: Safe session-based concurrency with shared linear state(artifact) (January 2023). https:\/\/doi.org\/10.5281\/zenodo.7506064","DOI":"10.5281\/zenodo.7506064"},{"key":"9_CR63","unstructured":"Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, USA (2001)"},{"key":"9_CR64","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A., Hao, K.: Safer smart contract programming with Scilla. Proc. ACM Program. Lang. 3(OOPSLA), 185:1\u2013185:30 (2019)","DOI":"10.1145\/3360611"},{"key":"9_CR65","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Functions as Session-Typed Processes. In: FoSSaCS\u201912. No.\u00a07213 in LNCS (2012)","DOI":"10.1007\/978-3-642-28729-9_23"},{"key":"9_CR66","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: A monadic integration. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. pp. 350\u2013369. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"9_CR67","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: A decade of dependent session types. In: Veltri, N., Benton, N., Ghilezan, S. (eds.) PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming. pp. 3:1\u20133:3. ACM (2021)","DOI":"10.1145\/3479394.3479398"},{"key":"9_CR68","doi-asserted-by":"crossref","unstructured":"Toninho, B., Yoshida, N.: On polymorphic sessions and functions: A tale of two (fully abstract) encodings. ACM Trans. Program. Lang. Syst. 43(2) (Jun 2021)","DOI":"10.1145\/3457884"},{"key":"9_CR69","unstructured":"Turner, D.N.: The polymorphic Pi-calculus : theory and implementation. Ph.D. thesis, University of Edinburgh, UK (1996)"},{"key":"9_CR70","doi-asserted-by":"crossref","unstructured":"Vasconcelos, V.T.: Lambda and pi calculi, CAM and SECD machines. J. Funct. Program. 15(1), 101\u2013127 (2005)","DOI":"10.1017\/S0956796804005386"},{"key":"9_CR71","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Propositions as sessions. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. p. 273\u2013286. ICFP \u201912, Association for Computing Machinery, New York, NY, USA (2012)","DOI":"10.1145\/2364527.2364568"},{"key":"9_CR72","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Propositions as Sessions. Journal of Functional Programming 24(2-3), 384\u2013418 (2014)","DOI":"10.1017\/S095679681400001X"},{"key":"9_CR73","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Propositions as Types. Commun. ACM 58(12), 75\u201384 (2015)","DOI":"10.1145\/2699407"},{"key":"9_CR74","doi-asserted-by":"crossref","unstructured":"Willsey, M., Prabhu, R., Pfenning, F.: Design and implementation of concurrent C0. In: Cervesato, I., Fern\u00e1ndez, M. (eds.) Proceedings Fourth International Workshop on Linearity, LINEARITY 2016. EPTCS, vol.\u00a0238, pp. 73\u201382 (2016)","DOI":"10.4204\/EPTCS.238.8"},{"key":"9_CR75","unstructured":"Wood, G.: Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum project yellow paper 151(2014), 1\u201332 (2014)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57262-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:15:58Z","timestamp":1731690958000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57262-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572616","9783031572623"],"references-count":75,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57262-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"An implementation of the SAM as a typechecker and interpreter is publicly available\u00a0[]. Additional definitions and proofs can be found in the companion extended technical report\u00a0[]","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"72","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also contain 4 artifact report that have not been part of the original submission","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}