{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:10Z","timestamp":1751660530012,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030992521"},{"type":"electronic","value":"9783030992538"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Many type systems include infinite types. In session type systems, infinite types are important because they specify communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions \"Equation missing\" or by non-parametric equational definitions \"Equation missing\". Alternatively, some systems of label- or value-dependent session types go beyond simple recursive types. However, leaving dependent types aside, there is a much richer world of infinite session types, ranging through various forms of parametric equational definitions, to arbitrary infinite types in a coinductively defined space. We study infinite session types across a spectrum of shades of grey on the way to the bright light of general infinite types. We identify four points on the spectrum, characterised by different styles of equational definitions, and show that they form a strict hierarchy by establishing bidirectional correspondences with classes of automata: finite-state, 1-counter, pushdown and 2-counter. This allows us to establish decidability and undecidability results for type formation, type equivalence and duality in each class of types. We also consider previous work on context-free session types (and extend it to higher-order) and nested session types, and locate them on our spectrum of infinite types.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_18","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"347-367","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The Different Shades of Infinite Session Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3033-9091","authenticated-orcid":false,"given":"Simon J.","family":"Gay","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5474-3614","authenticated-orcid":false,"given":"Diogo","family":"Po\u00e7as","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":[[2022,3,29]]},"reference":[{"key":"18_CR1","unstructured":"Almeida, B., Mordido, A., Thiemann, P., Vasconcelos, V.T.: Polymorphic context-free session types. CoRR abs\/2106.06658 (2021), https:\/\/arxiv.org\/abs\/2106.06658"},{"key":"18_CR2","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":"18_CR3","doi-asserted-by":"crossref","unstructured":"Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Sprachtypologie und Universalienforschung 14, 143\u2013172 (1961)","DOI":"10.1524\/stuf.1961.14.14.143"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Bergstra, J.A., Klop, J.W.: Process theory based on bisimulation semantics. In: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp. 50\u2013122. Springer (1988). https:\/\/doi.org\/10.1007\/BFb0013021","DOI":"10.1007\/BFb0013021"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types. Logical Methods in Computer Science 12(2) (2016). https:\/\/doi.org\/10.2168\/LMCS-12(2:10)2016","DOI":"10.2168\/LMCS-12(2:10)2016"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Bird, R.S., Meertens, L.G.L.T.: Nested datatypes. In: MPC. LNCS, vol.\u00a01422, pp. 52\u201367. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0054285","DOI":"10.1007\/BFb0054285"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Boasson, L.: Two iteration theorems for some families of languages. Journal of Computer and System Sciences 7(6), 583\u2013596 (1973)","DOI":"10.1016\/S0022-0000(73)80036-4"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"B\u00f6hm, S., G\u00f6ller, S., Jancar, P.: Equivalence of deterministic one-counter automata is nl-complete. In: STOC. pp. 131\u2013140. ACM (2013). https:\/\/doi.org\/10.1145\/2488608.2488626","DOI":"10.1145\/2488608.2488626"},{"key":"18_CR9","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":"18_CR10","unstructured":"Das, A., DeYoung, H., Mordido, A., Pfenning, F.: Subtyping on nested polymorphic session types. CoRR abs\/2103.15193 (2021), https:\/\/arxiv.org\/abs\/2103.15193"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Deni\u00e9lou, P., Yoshida, N.: Multiparty session types meet communicating automata. In: ESOP. LNCS, vol. 7211, pp. 194\u2013213. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_10","DOI":"10.1007\/978-3-642-28869-2_10"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Deni\u00e9lou, P., Yoshida, N., Bejleri, A., Hu, R.: Parameterised multiparty session types. Log. Methods Comput. Sci. 8(4) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(4:6)2012","DOI":"10.2168\/LMCS-8(4:6)2012"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Friedman, E.P.: The inclusion problem for simple languages. Theor. Comput. Sci. 1(4), 297\u2013316 (1976). https:\/\/doi.org\/10.1016\/0304-3975(76)90074-8","DOI":"10.1016\/0304-3975(76)90074-8"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Gapeyev, V., Levin, M.Y., Pierce, B.C.: Recursive subtyping revealed. J. Funct. Program. 12(6), 511\u2013548 (2002). https:\/\/doi.org\/10.1017\/S0956796802004318","DOI":"10.1017\/S0956796802004318"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2-3), 191\u2013225 (2005). https:\/\/doi.org\/10.1007\/s00236-005-0177-z","DOI":"10.1007\/s00236-005-0177-z"},{"key":"18_CR16","unstructured":"Gay, S.J., Po\u00e7as, D., Vasconcelos, V.T.: The different shades of infinite session types. CoRR abs\/2201.08275 (2022), https:\/\/arxiv.org\/abs\/2201.08275"},{"key":"18_CR17","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":"18_CR18","doi-asserted-by":"publisher","unstructured":"Groote, J.F., H\u00fcttel, H.: Undecidable equivalences for basic process algebra. Inf. Comput. 115(2), 354\u2013371 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1101","DOI":"10.1006\/inco.1994.1101"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Honda, K.: Types for dyadic interaction. In: CONCUR. LNCS, vol. 715, pp. 509\u2013523. Springer (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_35","DOI":"10.1007\/3-540-57208-2_35"},{"key":"18_CR20","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":"18_CR21","unstructured":"Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Tech. rep., Cornell University (1971)"},{"key":"18_CR22","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company (1979)"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"H\u00fcttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deni\u00e9lou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1\u20133:36 (2016). https:\/\/doi.org\/10.1145\/2873052","DOI":"10.1145\/2873052"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Kao, J.Y., Rampersad, N., Shallit, J.: On NFAs where all states are final, initial, or both. Theoretical Computer Science 410(47-49), 5010\u20135021 (2009)","DOI":"10.1016\/j.tcs.2009.07.049"},{"key":"18_CR25","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":"18_CR26","doi-asserted-by":"crossref","unstructured":"Kreowski, H.J.: A pumping lemma for context-free graph languages. In: International Workshop on Graph Grammars and Their Application to Computer Science. pp. 270\u2013283. Springer (1978)","DOI":"10.1007\/BFb0025726"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Lange, J., Yoshida, N.: Characteristic formulae for session types. In: TACAS. LNCS, vol. 9636, 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":"18_CR28","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":"18_CR29","doi-asserted-by":"publisher","unstructured":"de Muijnck-Hughes, J., Brady, E.C., Vanderbauwhede, W.: Value-dependent session design in a dependently typed language. In: PLACES. EPTCS, vol. 291, pp. 47\u201359 (2019). https:\/\/doi.org\/10.4204\/EPTCS.291.5","DOI":"10.4204\/EPTCS.291.5"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Mycroft, A.: Polymorphic type schemes and recursive definitions. In: International Symposium on Programming. LNCS, vol. 167, pp. 217\u2013228. Springer (1984). https:\/\/doi.org\/10.1007\/3-540-12925-1_41","DOI":"10.1007\/3-540-12925-1_41"},{"key":"18_CR31","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":"18_CR32","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press (2002)."},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM journal of research and development 3(2), 114\u2013125 (1959)","DOI":"10.1147\/rd.32.0114"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012). https:\/\/doi.org\/10.1017\/CBO9780511777110","DOI":"10.1017\/CBO9780511777110"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"S\u00e9nizergues, G.: The equivalence problem for deterministic pushdown automata is decidable. In: ICALP\u201997. LNCS, vol. 1256, pp. 671\u2013681. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63165-8_221","DOI":"10.1007\/3-540-63165-8_221"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"S\u00e9nizergues, G.: L (a)= l(b)? decidability results from complete formal systems. Theoretical Computer Science 251(1-2), 1\u2013166 (2001)","DOI":"10.1016\/S0304-3975(00)00285-1"},{"key":"18_CR37","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":"18_CR38","doi-asserted-by":"publisher","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: PARLE. LNCS, vol. 817, pp. 398\u2013413. Springer (1994). https:\/\/doi.org\/10.1007\/3-540-58184-7_118","DOI":"10.1007\/3-540-58184-7_118"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: ICFP. pp. 462\u2013475 (2016). https:\/\/doi.org\/10.1145\/2951913.2951926","DOI":"10.1145\/2951913.2951926"},{"key":"18_CR40","doi-asserted-by":"publisher","unstructured":"Thiemann, P., Vasconcelos, V.T.: Label-dependent session types. Proc. ACM Program. Lang. 4(POPL), 67:1\u201367:29 (2020). https:\/\/doi.org\/10.1145\/3371135","DOI":"10.1145\/3371135"},{"key":"18_CR41","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":"18_CR42","unstructured":"Valiant, L.G.: Decision procedures for families of deterministic pushdown automata. Ph.D. thesis, University of Warwick (1973)"},{"key":"18_CR43","doi-asserted-by":"crossref","unstructured":"Valiant, L.G., Paterson, M.S.: Deterministic one-counter automata. Journal of Computer and System Sciences 10(3), 340\u2013350 (1975)","DOI":"10.1016\/S0022-0000(75)80005-5"},{"key":"18_CR44","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":"18_CR45","doi-asserted-by":"publisher","unstructured":"Yoshida, N., Deni\u00e9lou, P., Bejleri, A., Hu, R.: Parameterised multiparty session types. In: FOSSACS. LNCS, vol. 6014, pp. 128\u2013145. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-12032-9_10","DOI":"10.1007\/978-3-642-12032-9_10"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:09:10Z","timestamp":1648498150000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","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":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"77","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":"23","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":"30% - 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":"9","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)"}}]}}