{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:06Z","timestamp":1775790726513,"version":"3.50.1"},"publisher-location":"Cham","reference-count":83,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031300431","type":"print"},{"value":"9783031300448","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"content-version":"vor","delay-in-days":106,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{CLASS}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>CLASS<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, a session-typed, higher-order, core language that supports concurrent computation with shared linear state.<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_16","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"421-450","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Safe Session-Based Concurrency with Shared Linear State"],"prefix":"10.1007","author":[{"given":"Pedro","family":"Rocha","sequence":"first","affiliation":[]},{"given":"Lu\u00eds","family":"Caires","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"16_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":"16_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":"16_CR3","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L$$^3$$: A linear language with locations. Fundam. Inf. 77(4), 397\u2013449 (Dec 2007)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 197\u2013347 (1992)","DOI":"10.1093\/logcom\/2.3.297"},{"key":"16_CR5","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":"16_CR6","doi-asserted-by":"crossref","unstructured":"Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Transactions on Computational Logic (TOCL) 3(1), 137\u2013175 (2002)","DOI":"10.1145\/504077.504081"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Atkey, R., Lindley, S., Morris, J.G.: Conflation confers concurrency. In: A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pp. 32\u201355. Springer (2016)","DOI":"10.1007\/978-3-319-30936-1_2"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Baelde, D.: Least and greatest fixed points in linear logic. TOCL 13(1) (Jan 2012)","DOI":"10.1145\/2071368.2071370"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Balzer, S., Pfenning, F.: Manifest sharing with session types. Proc. ACM Program. Lang. 1(ICFP) (Aug 2017)","DOI":"10.1145\/3110281"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Balzer, S., Toninho, B., Pfenning, F.: Manifest deadlock-freedom for shared session types. In: Caires, L. (ed.) Programming Languages and Systems. pp. 611\u2013639. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"16_CR11","unstructured":"Barber, A.: Dual Intuitionistic Linear Logic. Tech. Rep. LFCS-96-347, Univ. of Edinburgh (1996)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Beffara, E.: A Concurrent Model for Linear Logic. ENTCS 155, 147\u2013168 (2006)","DOI":"10.1016\/j.entcs.2005.11.055"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Beffara, E.: An algebraic process calculus. In: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science. p. 130\u2013141. LICS \u201908, IEEE Computer Society, USA (2008)","DOI":"10.1109\/LICS.2008.40"},{"key":"16_CR14","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":"16_CR15","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":"16_CR16","doi-asserted-by":"crossref","unstructured":"Boudol, G.: Typing termination in a higher-order concurrent imperative language. Information and Computation 208(6), 716\u2013736 (2010)","DOI":"10.1016\/j.ic.2009.06.007"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Brookes, S., O\u2019Hearn, P.W.: Concurrent Separation Logic. ACM SIGLOG News 3(3), 47\u201365 (2016)","DOI":"10.1145\/2984450.2984457"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Caires, L.: Logical Semantics of Types for Concurrency. In: International Conference on Algebra and Coalgebra in Computer Science. pp. 16\u201335. CALCO\u201907, Springer LNCS 4624 (2007)","DOI":"10.1007\/978-3-540-73859-6_2"},{"key":"16_CR19","unstructured":"Caires, L., P\u00e9rez, J.A., Pfenning, F., Toninho, B.: Relational parametricity for polymorphic session types. Tech. Rep. CMU-CS-12-108, Carnegie Mellon Univ. (2012)"},{"key":"16_CR20","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":"16_CR21","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":"16_CR22","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":"16_CR23","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-12. TLDI \u201912, Association for Computing Machinery, New York, NY, USA (2012)","DOI":"10.1145\/2103786.2103788"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Caires, L., Seco, J.a.C.: The type discipline of behavioral separation. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 275\u2013286. POPL \u201913, Association for Computing Machinery, New York, NY, USA (2013)","DOI":"10.1145\/2429069.2429103"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Caires, L., Vieira, H.T.: Conversation types. In: Castagna, G. (ed.) Programming Languages and Systems. pp. 285\u2013300. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-00590-9_21"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Caires, L., Vieira, H.T.: Conversation types. Theor. Comput. Sci. 411(51-52), 4399\u20134440 (2010)","DOI":"10.1016\/j.tcs.2010.09.010"},{"key":"16_CR27","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":"16_CR28","doi-asserted-by":"crossref","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured Interactional Exceptions in Session Types. In: CONCUR 2008. LNCS, vol.\u00a05201, pp. 402\u2013417. Springer (2008)","DOI":"10.1007\/978-3-540-85361-9_32"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Computing Surveys (CSUR) 17(4), 471\u2013523 (1985)","DOI":"10.1145\/6041.6042"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. p. 48\u201364. OOPSLA \u201998, Association for Computing Machinery, New York, NY, USA (1998)","DOI":"10.1145\/286936.286947"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Dardha, O., Gay, S.J.: A new linear logic for deadlock-free session-typed processes. In: Baier, C., Dal\u00a0Lago, U. (eds.) Foundations of Software Science and Computation Structures. pp. 91\u2013109. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Demangeon, R., Hirschkoff, D., Sangiorgi, D.: Mobile processes and termination. In: Semantics and Algebraic Specification, pp. 250\u2013273. Springer (2009)","DOI":"10.1007\/978-3-642-04164-8_13"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Dezani-Ciancaglini, M., de\u2019Liguoro, U., Yoshida, N.: On progress for structured communications. In: Barthe, G., Fournet, C. (eds.) Trustworthy Global Computing. pp. 257\u2013275. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78663-4_18"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequential processes. In: The origin of concurrent programming, pp. 198\u2013227. Springer (1971)","DOI":"10.1007\/978-1-4757-3472-0_5"},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Ehrhard, T.: An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28(7), 995\u20131060 (2018)","DOI":"10.1017\/S0960129516000372"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Fowler, S., Lindley, S., Morris, J.G., Decova, S.: Exceptional asynchronous session types: session types without tiers. Proceedings of the ACM on Programming Languages 3(POPL), 1\u201329 (2019)","DOI":"10.1145\/3290341"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1\u2013102 (1987)","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Linear logic. Theoretical computer science 50(1), 1\u2013101 (1987)","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Monitors: An operating system structuring concept. Commun. ACM 17(10), 549\u2013557 (1974)","DOI":"10.1145\/355620.361161"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. In: The origin of concurrent programming, pp. 231\u2013244. Springer (1972)","DOI":"10.1007\/978-1-4757-3472-0_6"},{"key":"16_CR41","doi-asserted-by":"crossref","unstructured":"Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and computation 110(2), 327\u2013365 (1994)","DOI":"10.1006\/inco.1994.1036"},{"key":"16_CR42","unstructured":"Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press (1980)"},{"key":"16_CR43","doi-asserted-by":"crossref","unstructured":"Jacobs, J., Balzer, S.: Higher-order leak and deadlock free locks. Proceedings of the ACM on Programming Languages 7(POPL), 1027\u20131057 (2023)","DOI":"10.1145\/3571229"},{"key":"16_CR44","doi-asserted-by":"crossref","unstructured":"Jacobs, J., Balzer, S., Krebbers, R.: Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang. 6(POPL), 1\u201333 (2022)","DOI":"10.1145\/3498662"},{"key":"16_CR45","doi-asserted-by":"crossref","unstructured":"Jones, S.P., Gordon, A., Finne, S.: Concurrent Haskell. In: POPL. vol.\u00a096, pp. 295\u2013308. Citeseer (1996)","DOI":"10.1145\/237721.237794"},{"key":"16_CR46","unstructured":"Klabnik, S., Nichols, C.: The Rust Programming Language (2021)"},{"key":"16_CR47","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: A type system for lock-free processes. Information and Computation 177(2), 122\u2013159 (2002)","DOI":"10.1006\/inco.2002.3171"},{"key":"16_CR48","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: A new type system for deadlock-free processes. In: International Conference on Concurrency Theory. pp. 233\u2013247. Springer (2006)","DOI":"10.1007\/11817949_16"},{"key":"16_CR49","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sangiorgi, D.: A hybrid type system for lock-freedom of mobile processes. ACM Transactions on Programming Languages and Systems (TOPLAS) 32(5), 1\u201349 (2008)","DOI":"10.1145\/1745312.1745313"},{"key":"16_CR50","doi-asserted-by":"crossref","unstructured":"Kokke, W., Morris, J.G., Wadler, P.: Towards races in linear logic. In: Riis\u00a0Nielson, H., Tuosto, E. (eds.) Coordination Models and Languages. pp. 37\u201353. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-22397-7_3"},{"key":"16_CR51","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Pradic, P., Benton, N.: Integrating linear and dependent types. ACM SIGPLAN Notices 50(1), 17\u201330 (2015)","DOI":"10.1145\/2775051.2676969"},{"key":"16_CR52","unstructured":"Lagaillardie, N., Neykova, R., Yoshida, N.: Stay safe under panic: Affine rust programming with multiparty session types. arXiv preprint arXiv:2204.13464 (2022)"},{"key":"16_CR53","unstructured":"Lea, D.: Concurrent programming in Java: design principles and patterns. Addison-Wesley Professional (2000)"},{"key":"16_CR54","doi-asserted-by":"crossref","unstructured":"Lindley, S., Morris, J.G.: Talking bananas: structural recursion for session types. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. pp. 434\u2013447. ACM (2016)","DOI":"10.1145\/3022670.2951921"},{"key":"16_CR55","doi-asserted-by":"crossref","unstructured":"Lynch, N.A.: Fast allocation of nearby resources in a distributed system. In: Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing. p. 70\u201381. STOC \u201980, Association for Computing Machinery, New York, NY, USA (1980)","DOI":"10.1145\/800141.804654"},{"key":"16_CR56","doi-asserted-by":"crossref","unstructured":"Marlow, S.: Parallel and concurrent programming in Haskell: Techniques for multicore and multithreaded programming. \" O\u2019Reilly Media, Inc.\" (2013)","DOI":"10.1007\/978-3-642-32096-5_7"},{"key":"16_CR57","doi-asserted-by":"crossref","unstructured":"Milit\u00e3o, F., Aldrich, J., Caires, L.: Aliasing control with view-based typestate. In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs. pp.\u00a01\u20137 (2010)","DOI":"10.1145\/1924520.1924527"},{"key":"16_CR58","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems (TOPLAS) 10(3), 470\u2013502 (1988)","DOI":"10.1145\/44501.45065"},{"key":"16_CR59","doi-asserted-by":"crossref","unstructured":"Mostrous, D., Vasconcelos, V.T.: Affine Sessions. In: Proc. of COORDINATION 2014. LNCS, vol.\u00a08459, pp. 115\u2013130. Springer (2014)","DOI":"10.1007\/978-3-662-43376-8_8"},{"key":"16_CR60","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, J.G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5-6), 865\u2013911 (2008)","DOI":"10.1017\/S0956796808006953"},{"key":"16_CR61","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C.: From Algol to polymorphic linear lambda-calculus. J. ACM 47(1), 167\u2013223 (2000)","DOI":"10.1145\/331605.331611"},{"key":"16_CR62","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":"16_CR63","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":"16_CR64","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":"16_CR65","unstructured":"Rocha, P.: A Logical Foundation for Session-Based Concurrent Computation. Ph.D. thesis, NOVA School of Science and Technology (July 2022)"},{"key":"16_CR66","doi-asserted-by":"crossref","unstructured":"Rocha, P., Caires, L.: A Propositions-as-Types System for Shared State. Tech. rep., NOVA Laboratory for Computer Science and Informatics (06 2021)","DOI":"10.1145\/3473584"},{"key":"16_CR67","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":"16_CR68","doi-asserted-by":"publisher","unstructured":"Rocha, P., Caires, L.: Safe ssession-based concurrency with shared linear state (artifact) (January 2023). https:\/\/doi.org\/10.5281\/zenodo.7506064","DOI":"10.5281\/zenodo.7506064"},{"key":"16_CR69","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: Termination of processes. Math. Struct. in Comp. Sci. 16(1), 1\u201339 (2006)","DOI":"10.1017\/S0960129505004810"},{"key":"16_CR70","unstructured":"Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, USA (2001)"},{"key":"16_CR71","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming. p. 161\u2013172. PPDP \u201911, Association for Computing Machinery, New York, NY, USA (2011)","DOI":"10.1145\/2003476.2003499"},{"key":"16_CR72","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Corecursion and non-divergence in session-typed processes. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. Lecture Notes in Computer Science, vol.\u00a08902, pp. 159\u2013175. Springer (2014)","DOI":"10.1007\/978-3-662-45917-1_11"},{"key":"16_CR73","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Corecursion and non-divergence in session-typed processes. In: International Symposium on Trustworthy Global Computing. pp. 159\u2013175. Springer (2014)","DOI":"10.1007\/978-3-662-45917-1_11"},{"key":"16_CR74","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":"16_CR75","doi-asserted-by":"crossref","unstructured":"Tov, J.A., Pucella, R.: Practical Affine Types. In: POPL 2011. pp. 447\u2013458 (2011)","DOI":"10.1145\/1925844.1926436"},{"key":"16_CR76","doi-asserted-by":"crossref","unstructured":"Vieira, H.T., Vasconcelos, V.T.: Typing progress in communication-centred systems. In: International Conference on Coordination Languages and Models. pp. 236\u2013250. Springer (2013)","DOI":"10.1007\/978-3-642-38493-6_17"},{"key":"16_CR77","doi-asserted-by":"crossref","unstructured":"Voinea, A.L., Dardha, O., Gay, S.J.: Resource sharing via capability-based multiparty session types. In: International Conference on Integrated Formal Methods. pp. 437\u2013455. Springer (2019)","DOI":"10.1007\/978-3-030-34968-4_24"},{"key":"16_CR78","unstructured":"Wadler, P.: Linear types can change the world! In: Broy, M. (ed.) Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, 1990. p.\u00a0561. North-Holland (1990)"},{"key":"16_CR79","unstructured":"Wadler, P.: Recursive types for free (1990)"},{"key":"16_CR80","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":"16_CR81","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":"16_CR82","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Propositions as types. Communications of the ACM 58(12), 75\u201384 (2015)","DOI":"10.1145\/2699407"},{"key":"16_CR83","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the $$\\pi $$-calculus. Information and Computation 191(2), 145\u2013202 (2004)","DOI":"10.1016\/j.ic.2003.08.004"}],"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-30044-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T10:38:56Z","timestamp":1729247936000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/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":"55","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":"20","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":"0","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":"36% - 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","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":"5.5","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)"}}]}}