{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:38Z","timestamp":1775790818012,"version":"3.50.1"},"publisher-location":"Cham","reference-count":74,"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 study increasingly expressive type systems, from<jats:inline-formula><jats:alternatives><jats:tex-math>$$F^\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mi>F<\/mml:mi><mml:mi>\u03bc<\/mml:mi><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u2014an extension of the polymorphic lambda calculus with equirecursive types\u2014to<jats:inline-formula><jats:alternatives><jats:tex-math>$$F^{\\mu ;}_\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msubsup><mml:mi>F<\/mml:mi><mml:mi>\u03c9<\/mml:mi><mml:mrow><mml:mi>\u03bc<\/mml:mi><mml:mo>\u037e<\/mml:mo><\/mml:mrow><\/mml:msubsup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u2014the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contractive fragment of<jats:inline-formula><jats:alternatives><jats:tex-math>$$F^\\mu _\\omega $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msubsup><mml:mi>F<\/mml:mi><mml:mi>\u03c9<\/mml:mi><mml:mi>\u03bc<\/mml:mi><\/mml:msubsup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>as studied in the literature. Decidability results for type equivalence of the various type languages are obtained from the translation of types into objects of an appropriate computational model: finite-state automata, simple grammars and deterministic pushdown automata. We show that type equivalence is decidable for a significant fragment of the type language. We further propose a message-passing, concurrent functional language equipped with the expressive type language and show that it enjoys preservation and absence of runtime errors for typable processes.<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_15","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"392-420","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["System $$F^\\mu _\\omega $$ with Context-free Session Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5474-3614","authenticated-orcid":false,"given":"Diogo","family":"Po\u00e7as","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8312-429X","authenticated-orcid":false,"given":"Diana","family":"Costa","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1547-0692","authenticated-orcid":false,"given":"Andreia","family":"Mordido","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9539-8861","authenticated-orcid":false,"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"15_CR1","unstructured":"Abel, A.: Type-based termination: a polymorphic lambda-calculus with sized higher-order types. Ph.D. thesis, Ludwig Maximilians University Munich (2007), https:\/\/d-nb.info\/984765581"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Almeida, B., Mordido, A., Thiemann, P., Vasconcelos, V.T.: Polymorphic lambda calculus with context-free session types. Inf. Comput. 289(Part), 104948 (2022). https:\/\/doi.org\/10.1016\/j.ic.2022.104948","DOI":"10.1016\/j.ic.2022.104948"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Almeida, B., Mordido, A., Vasconcelos, V.T.: FreeST: Context-free session types in a functional language. In: PLACES. EPTCS, vol.\u00a0291, pp. 12\u201323 (2019). https:\/\/doi.org\/10.4204\/EPTCS.291.2","DOI":"10.4204\/EPTCS.291.2"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Almeida, B., Mordido, A., Vasconcelos, V.T.: Deciding the bisimilarity of context-free session types. In: TACAS. LNCS, vol. 12079, pp. 39\u201356. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_3","DOI":"10.1007\/978-3-030-45237-7_3"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Amadio, R.M., Cardelli, L.: Subtyping recursive types. In: POPL. pp. 104\u2013118. ACM Press (1991). https:\/\/doi.org\/10.1145\/99583.99600","DOI":"10.1145\/99583.99600"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Decidability of bisimulation equivalence for processes generating context-free languages. In: PARLE. LNCS, vol.\u00a0259, pp. 94\u2013111. Springer (1987). https:\/\/doi.org\/10.1007\/3-540-17945-3_5","DOI":"10.1007\/3-540-17945-3_5"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Decidability of bisimulation equivalence for processes generating context-free languages. J. ACM 40(3), 653\u2013682 (1993). https:\/\/doi.org\/10.1145\/174130.174141","DOI":"10.1145\/174130.174141"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Balzer, S., Pfenning, F.: Manifest sharing with session types. Proc. ACM Program. Lang. 1(ICFP), 37:1\u201337:29 (2017). https:\/\/doi.org\/10.1145\/3110281","DOI":"10.1145\/3110281"},{"key":"15_CR9","unstructured":"Barendregt, H.P.: The lambda calculus - its syntax and semantics, Studies in logic and the foundations of mathematics, vol.\u00a0103. North-Holland (1985)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P.: The type free lambda calculus. In: Studies in Logic and the Foundations of Mathematics, vol.\u00a090, pp. 1091\u20131132. Elsevier (1977)","DOI":"10.1016\/S0049-237X(08)71129-7"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundam. Informaticae 33(4), 309\u2013338 (1998). https:\/\/doi.org\/10.3233\/FI-1998-33401","DOI":"10.3233\/FI-1998-33401"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing object encodings. In: TACS. LNCS, vol.\u00a01281, pp. 415\u2013438. Springer (1997). https:\/\/doi.org\/10.1007\/BFb0014561","DOI":"10.1007\/BFb0014561"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Burkart, O., Caucal, D., Steffen, B.: An elementary bisimulation decision procedure for arbitrary context-free processes. In: MFCS. LNCS, vol.\u00a0969, pp. 423\u2013433. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-60246-1_148","DOI":"10.1007\/3-540-60246-1_148"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Cai, Y., Giarrusso, P.G., Ostermann, K.: System F-omega with equirecursive types for datatype-generic programming. In: POPL. pp. 30\u201343. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837660","DOI":"10.1145\/2837614.2837660"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Caires, L., P\u00e9rez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: ESOP. LNCS, vol.\u00a07792, pp. 330\u2013349. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_19","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"15_CR16","doi-asserted-by":"publisher","unstructured":"Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471\u2013522 (1985). https:\/\/doi.org\/10.1145\/6041.6042","DOI":"10.1145\/6041.6042"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Christensen, S., H\u00fcttel, H., Stirling, C.: Bisimulation equivalence is decidable for all context-free processes. Inf. Comput. 121(2), 143\u2013148 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1129","DOI":"10.1006\/inco.1995.1129"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Colazzo, D., Ghelli, G.: Subtyping recursive types in kernel Fun. In: LICS. pp. 137\u2013146. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782605","DOI":"10.1109\/LICS.1999.782605"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Costa, D., Mordido, A., Po\u00e7as, D., Vasconcelos, V.T.: Higher-order context-free session types in system F. In: PLACES. EPTCS, vol.\u00a0356, pp. 24\u201335 (2022). https:\/\/doi.org\/10.4204\/EPTCS.356.3","DOI":"10.4204\/EPTCS.356.3"},{"key":"15_CR20","unstructured":"Costa, D., Mordido, A., Po\u00e7as, D., Vasconcelos, V.T.: System $$F^{\\mu }_{\\omega }$$ with context-free session types. CoRR abs\/2301.08659 (2023), http:\/\/arxiv.org\/abs\/2301.08659"},{"key":"15_CR21","unstructured":"Curry, H.H., Feys, R., Craig, W. (eds.): Combinatory Logic, Volume I. North-Holland (1958)"},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Dardha, O.: Recursive session types revisited. In: BEAT. EPTCS, vol.\u00a0162, pp. 27\u201334 (2014). https:\/\/doi.org\/10.4204\/EPTCS.162.4","DOI":"10.4204\/EPTCS.162.4"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253\u2013286 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.06.002","DOI":"10.1016\/j.ic.2017.06.002"},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Das, A., DeYoung, H., Mordido, A., Pfenning, F.: Nested session types. In: ESOP. LNCS, vol. 12648, pp. 178\u2013206. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_7","DOI":"10.1007\/978-3-030-72019-3_7"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Das, A., DeYoung, H., Mordido, A., Pfenning, F.: Nested session types. ACM Trans. Program. Lang. Syst. 44(3), 19:1\u201319:45 (2022). https:\/\/doi.org\/10.1145\/3539656","DOI":"10.1145\/3539656"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Das, A., Pfenning, F.: Rast: A language for resource-aware session types. Log. Methods Comput. Sci. 18(1) (2022). https:\/\/doi.org\/10.46298\/lmcs-18(1:9)2022","DOI":"10.46298\/lmcs-18(1:9)2022"},{"key":"15_CR27","doi-asserted-by":"publisher","unstructured":"De\u00a0Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae. vol.\u00a075, pp. 381\u2013392. Elsevier (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"15_CR28","unstructured":"The FreeST programming language. https:\/\/freest-lang.github.io\/ (2019)"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Gapeyev, V., Levin, M.Y., Pierce, B.C.: Recursive subtyping revealed: functional pearl. In: ICFP. pp. 221\u2013231. ACM (2000). https:\/\/doi.org\/10.1145\/351240.351261","DOI":"10.1145\/351240.351261"},{"key":"15_CR30","doi-asserted-by":"publisher","unstructured":"Gauthier, N., Pottier, F.: Numbering matters: first-order canonical forms for second-order recursive types. In: ICFP. pp. 150\u2013161. ACM (2004). https:\/\/doi.org\/10.1145\/1016850.1016872","DOI":"10.1145\/1016850.1016872"},{"key":"15_CR31","doi-asserted-by":"publisher","unstructured":"Gay, S.J.: Bounded polymorphism in session types. MSCS 18(5), 895\u2013930 (2008). https:\/\/doi.org\/10.1017\/S0960129508006944","DOI":"10.1017\/S0960129508006944"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2-3), 191\u2013225 (2005). https:\/\/doi.org\/10.1007\/s00236-005-0177-z","DOI":"10.1007\/s00236-005-0177-z"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Po\u00e7as, D., Vasconcelos, V.T.: The different shades of infinite session types. In: FoSSaCS. LNCS, vol. 13242, pp. 347\u2013367. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_18","DOI":"10.1007\/978-3-030-99253-8_18"},{"key":"15_CR34","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Thiemann, P., Vasconcelos, V.T.: Duality of session types: The final cut. In: PLACES. EPTCS, vol.\u00a0314, pp. 23\u201333 (2020). https:\/\/doi.org\/10.4204\/EPTCS.314.3","DOI":"10.4204\/EPTCS.314.3"},{"key":"15_CR35","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19\u201350 (2010). https:\/\/doi.org\/10.1017\/S0956796809990268","DOI":"10.1017\/S0956796809990268"},{"key":"15_CR36","unstructured":"Girard, J.Y.: Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph.D. thesis, \u00c9diteur inconnu (1972)"},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Glew, N.: A theory of second-order trees. In: ESOP. LNCS, vol.\u00a02305, pp. 147\u2013161. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45927-8_11","DOI":"10.1007\/3-540-45927-8_11"},{"key":"15_CR39","doi-asserted-by":"publisher","unstructured":"Griffith, D.E.: Polarized substructural session types. Ph.D. thesis, University of Illinois at Urbana-Champaign (2016). https:\/\/doi.org\/10.2172\/1562827","DOI":"10.2172\/1562827"},{"key":"15_CR40","unstructured":"Hindley, J.R., Seldin, J.P.: Introduction to Combinators and Lambda-Calculus. Cambridge University Press (1986)"},{"key":"15_CR41","doi-asserted-by":"publisher","unstructured":"Hinze, R.: Polytypic values possess polykinded types. Sci. Comput. Program. 43(2-3), 129\u2013159 (2002). https:\/\/doi.org\/10.1016\/S0167-6423(02)00025-4","DOI":"10.1016\/S0167-6423(02)00025-4"},{"key":"15_CR42","doi-asserted-by":"publisher","unstructured":"Honda, K.: Types for dyadic interaction. In: CONCUR. LNCS, vol.\u00a0715, pp. 509\u2013523. Springer (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_35","DOI":"10.1007\/3-540-57208-2_35"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: ESOP. LNCS, vol.\u00a01381, pp. 122\u2013138. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0053567","DOI":"10.1007\/BFb0053567"},{"key":"15_CR44","unstructured":"Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Tech. rep., Cornell University (1971)"},{"key":"15_CR45","doi-asserted-by":"publisher","unstructured":"Im, H., Nakata, K., Park, S.: Contractive signatures with recursive types, type parameters, and abstract types. In: ICALP. LNCS, vol.\u00a07966, pp. 299\u2013311. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_28","DOI":"10.1007\/978-3-642-39212-2_28"},{"key":"15_CR46","unstructured":"Jan\u010dar, P.: Short decidability proof for DPDA language equivalence via 1st order grammar bisimilarity. CoRR abs\/1010.4760 (2010), http:\/\/arxiv.org\/abs\/1010.4760"},{"key":"15_CR47","doi-asserted-by":"publisher","unstructured":"Jan\u010dar, P.: Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof). Log. Methods Comput. Sci. 9(1) (2012). https:\/\/doi.org\/10.2168\/LMCS-9(1:10)2013","DOI":"10.2168\/LMCS-9(1:10)2013"},{"key":"15_CR48","doi-asserted-by":"publisher","unstructured":"Keizer, A.C., Basold, H., P\u00e9rez, J.A.: Session coalgebras: A coalgebraic view on session types and communication protocols. In: ESOP. LNCS, vol. 12648, pp. 375\u2013403. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_14","DOI":"10.1007\/978-3-030-72019-3_14"},{"key":"15_CR49","doi-asserted-by":"publisher","unstructured":"Kiefer, S.: BPA bisimilarity is EXPTIME-hard. Inf. Process. Lett. 113(4), 101\u2013106 (2013). https:\/\/doi.org\/10.1016\/j.ipl.2012.12.004","DOI":"10.1016\/j.ipl.2012.12.004"},{"key":"15_CR50","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914\u2013947 (1999). https:\/\/doi.org\/10.1145\/330249.330251","DOI":"10.1145\/330249.330251"},{"key":"15_CR51","doi-asserted-by":"publisher","unstructured":"Korenjak, A.J., Hopcroft, J.E.: Simple deterministic languages. In: SWAT. pp. 36\u201346. IEEE Computer Society (1966). https:\/\/doi.org\/10.1109\/SWAT.1966.22","DOI":"10.1109\/SWAT.1966.22"},{"key":"15_CR52","doi-asserted-by":"publisher","unstructured":"Kozen, D., Silva, A.: Practical coinduction. Math. Struct. Comput. Sci. 27(7), 1132\u20131152 (2017). https:\/\/doi.org\/10.1017\/S0960129515000493","DOI":"10.1017\/S0960129515000493"},{"key":"15_CR53","doi-asserted-by":"publisher","unstructured":"Lange, J., Yoshida, N.: Characteristic formulae for session types. In: TACAS. LNCS, vol.\u00a09636, pp. 833\u2013850. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_52","DOI":"10.1007\/978-3-662-49674-9_52"},{"key":"15_CR54","doi-asserted-by":"publisher","unstructured":"Lindley, S., Morris, J.G.: Talking bananas: structural recursion for session types. In: ICFP. pp. 434\u2013447. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951921","DOI":"10.1145\/2951913.2951921"},{"key":"15_CR55","doi-asserted-by":"publisher","unstructured":"Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119\u2013141 (1992). https:\/\/doi.org\/10.1017\/S0960129500001407","DOI":"10.1017\/S0960129500001407"},{"key":"15_CR56","doi-asserted-by":"publisher","unstructured":"Padovani, L.: Context-free session type inference. ACM Trans. Program. Lang. Syst. 41(2), 9:1\u20139:37 (2019). https:\/\/doi.org\/10.1145\/3229062","DOI":"10.1145\/3229062"},{"key":"15_CR57","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press (2002)"},{"key":"15_CR58","doi-asserted-by":"publisher","unstructured":"Puntigam, F.: Non-regular process types. In: Euro-Par. LNCS, vol.\u00a01685, pp. 1334\u20131343. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48311-X_189","DOI":"10.1007\/3-540-48311-X_189"},{"key":"15_CR59","doi-asserted-by":"publisher","unstructured":"Ravara, A., Vasconcelos, V.T.: Behavioural types for a calculus of concurrent objects. In: Euro-Par. LNCS, vol.\u00a01300, pp. 554\u2013561. Springer (1997). https:\/\/doi.org\/10.1007\/BFb0002782","DOI":"10.1007\/BFb0002782"},{"key":"15_CR60","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Towards a theory of type structure. In: Programming Symposium. LNCS, vol.\u00a019, pp. 408\u2013423. Springer (1974). https:\/\/doi.org\/10.1007\/3-540-06859-7_148","DOI":"10.1007\/3-540-06859-7_148"},{"key":"15_CR61","doi-asserted-by":"publisher","unstructured":"S\u00e9nizergues, G.: The equivalence problem for deterministic pushdown automata is decidable. In: ICALP. LNCS, vol.\u00a01256, pp. 671\u2013681. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63165-8_221","DOI":"10.1007\/3-540-63165-8_221"},{"key":"15_CR62","doi-asserted-by":"publisher","unstructured":"S\u00e9nizergues, G.: L(A) = L(B)? decidability results from complete formal systems. In: ICALP. LNCS, vol.\u00a02380, p.\u00a037. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45465-9_4","DOI":"10.1007\/3-540-45465-9_4"},{"key":"15_CR63","doi-asserted-by":"publisher","unstructured":"Solomon, M.H.: Type definitions with parameters. In: POPL. pp. 31\u201338. ACM Press (1978). https:\/\/doi.org\/10.1145\/512760.512765","DOI":"10.1145\/512760.512765"},{"key":"15_CR64","doi-asserted-by":"publisher","unstructured":"Stirling, C.: Decidability of DPDA equivalence. Theor. Comput. Sci. 255(1-2), 1\u201331 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00389-3","DOI":"10.1016\/S0304-3975(00)00389-3"},{"key":"15_CR65","doi-asserted-by":"publisher","unstructured":"Stirling, C.: Deciding DPDA equivalence is primitive recursive. In: ICALP. Lecture Notes in Computer Science, vol.\u00a02380, pp. 821\u2013832. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45465-9_70","DOI":"10.1007\/3-540-45465-9_70"},{"key":"15_CR66","doi-asserted-by":"publisher","unstructured":"S\u00fcdholt, M.: A model of components with non-regular protocols. In: SC. LNCS, vol.\u00a03628, pp. 99\u2013113. Springer (2005). https:\/\/doi.org\/10.1007\/11550679_8","DOI":"10.1007\/11550679_8"},{"key":"15_CR67","doi-asserted-by":"publisher","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: PARLE. LNCS, vol.\u00a0817, pp. 398\u2013413. Springer (1994). https:\/\/doi.org\/10.1007\/3-540-58184-7_118","DOI":"10.1007\/3-540-58184-7_118"},{"key":"15_CR68","doi-asserted-by":"publisher","unstructured":"Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: ICFP. pp. 462\u2013475. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951926","DOI":"10.1145\/2951913.2951926"},{"key":"15_CR69","doi-asserted-by":"publisher","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP. pp. 161\u2013172. ACM (2011). https:\/\/doi.org\/10.1145\/2003476.2003499","DOI":"10.1145\/2003476.2003499"},{"key":"15_CR70","doi-asserted-by":"publisher","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: A monadic integration. In: ESOP. LNCS, vol.\u00a07792, pp. 350\u2013369. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_20","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"15_CR71","doi-asserted-by":"publisher","unstructured":"Toninho, B., Yoshida, N.: On polymorphic sessions and functions: A tale of two (fully abstract) encodings. ACM Trans. Program. Lang. Syst. 43(2), 7:1\u20137:55 (2021). https:\/\/doi.org\/10.1145\/3457884","DOI":"10.1145\/3457884"},{"key":"15_CR72","unstructured":"Tov, J.A.: Practical programming with substructural types. Ph.D. thesis, Northeastern University (2012)"},{"key":"15_CR73","doi-asserted-by":"publisher","unstructured":"Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52\u201370 (2012). https:\/\/doi.org\/10.1016\/j.ic.2012.05.002","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"15_CR74","doi-asserted-by":"crossref","unstructured":"Walker, D.: Advanced Topics in Types and Programming Languages, chap. Substructural Type Systems, pp. 3\u201344. The MIT Press (2005)","DOI":"10.7551\/mitpress\/1104.003.0003"}],"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_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T10:38:44Z","timestamp":1729247924000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_15","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)"}}]}}