Abstract
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 
or by non-parametric equational definitions 
. 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.
Supported by EPSRC EP/T014628/1 “Session Types for Reliable Distributed Systems”, by FCT PTDC/CCI-CIF/6453/2020 “Safe Concurrent Programming with Session Types”, and by the LASIGE Research Unit UIDB/00408/2020 and UIDP/00408/2020. A full version is available at https://arxiv.org/abs/2201.08275 [16].
Chapter PDF
Similar content being viewed by others
References
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
Almeida, B., Mordido, A., Vasconcelos, V.T.: Deciding the bisimilarity of context-free session types. In: TACAS. LNCS, vol. 12079, pp. 39–56. Springer (2020). https://doi.org/10.1007/978-3-030-45237-7_3
Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Sprachtypologie und Universalienforschung 14, 143–172 (1961)
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. 354, pp. 50–122. Springer (1988). https://doi.org/10.1007/BFb0013021
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
Bird, R.S., Meertens, L.G.L.T.: Nested datatypes. In: MPC. LNCS, vol. 1422, pp. 52–67. Springer (1998). https://doi.org/10.1007/BFb0054285
Boasson, L.: Two iteration theorems for some families of languages. Journal of Computer and System Sciences 7(6), 583–596 (1973)
Böhm, S., Göller, S., Jancar, P.: Equivalence of deterministic one-counter automata is nl-complete. In: STOC. pp. 131–140. ACM (2013). https://doi.org/10.1145/2488608.2488626
Das, A., DeYoung, H., Mordido, A., Pfenning, F.: Nested session types. In: ESOP. LNCS, vol. 12648, pp. 178–206. Springer (2021). https://doi.org/10.1007/978-3-030-72019-3_7
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
Deniélou, P., Yoshida, N.: Multiparty session types meet communicating automata. In: ESOP. LNCS, vol. 7211, pp. 194–213. Springer (2012). https://doi.org/10.1007/978-3-642-28869-2_10
Deniélou, 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
Friedman, E.P.: The inclusion problem for simple languages. Theor. Comput. Sci. 1(4), 297–316 (1976). https://doi.org/10.1016/0304-3975(76)90074-8
Gapeyev, V., Levin, M.Y., Pierce, B.C.: Recursive subtyping revealed. J. Funct. Program. 12(6), 511–548 (2002). https://doi.org/10.1017/S0956796802004318
Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2-3), 191–225 (2005). https://doi.org/10.1007/s00236-005-0177-z
Gay, S.J., Poças, D., Vasconcelos, V.T.: The different shades of infinite session types. CoRR abs/2201.08275 (2022), https://arxiv.org/abs/2201.08275
Gay, S.J., Thiemann, P., Vasconcelos, V.T.: Duality of session types: The final cut. In: PLACES. EPTCS, vol. 314, pp. 23–33 (2020). https://doi.org/10.4204/EPTCS.314.3
Groote, J.F., Hüttel, H.: Undecidable equivalences for basic process algebra. Inf. Comput. 115(2), 354–371 (1994). https://doi.org/10.1006/inco.1994.1101
Honda, K.: Types for dyadic interaction. In: CONCUR. LNCS, vol. 715, pp. 509–523. Springer (1993). https://doi.org/10.1007/3-540-57208-2_35
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: ESOP. LNCS, vol. 1381, pp. 122–138. Springer (1998). https://doi.org/10.1007/BFb0053567
Hopcroft, J.E., Karp, R.M.: A linear algorithm for testing equivalence of finite automata. Tech. rep., Cornell University (1971)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Publishing Company (1979)
Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, 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–3:36 (2016). https://doi.org/10.1145/2873052
Kao, J.Y., Rampersad, N., Shallit, J.: On NFAs where all states are final, initial, or both. Theoretical Computer Science 410(47-49), 5010–5021 (2009)
Keizer, A.C., Basold, H., Pérez, J.A.: Session coalgebras: A coalgebraic view on session types and communication protocols. In: ESOP. LNCS, vol. 12648, pp. 375–403. Springer (2021). https://doi.org/10.1007/978-3-030-72019-3_14
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–283. Springer (1978)
Lange, J., Yoshida, N.: Characteristic formulae for session types. In: TACAS. LNCS, vol. 9636, pp. 833–850. Springer (2016). https://doi.org/10.1007/978-3-662-49674-9_52
Lindley, S., Morris, J.G.: Talking bananas: structural recursion for session types. In: ICFP. pp. 434–447. ACM (2016). https://doi.org/10.1145/2951913.2951921
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–59 (2019). https://doi.org/10.4204/EPTCS.291.5
Mycroft, A.: Polymorphic type schemes and recursive definitions. In: International Symposium on Programming. LNCS, vol. 167, pp. 217–228. Springer (1984). https://doi.org/10.1007/3-540-12925-1_41
Padovani, L.: Context-free session type inference. ACM Trans. Program. Lang. Syst. 41(2), 9:1–9:37 (2019). https://doi.org/10.1145/3229062
Pierce, B.C.: Types and programming languages. MIT Press (2002).
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM journal of research and development 3(2), 114–125 (1959)
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012). https://doi.org/10.1017/CBO9780511777110
Sénizergues, G.: The equivalence problem for deterministic pushdown automata is decidable. In: ICALP’97. LNCS, vol. 1256, pp. 671–681. Springer (1997). https://doi.org/10.1007/3-540-63165-8_221
Sénizergues, G.: L (a)= l(b)? decidability results from complete formal systems. Theoretical Computer Science 251(1-2), 1–166 (2001)
Solomon, M.H.: Type definitions with parameters. In: POPL. pp. 31–38. ACM Press (1978). https://doi.org/10.1145/512760.512765
Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: PARLE. LNCS, vol. 817, pp. 398–413. Springer (1994). https://doi.org/10.1007/3-540-58184-7_118
Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: ICFP. pp. 462–475 (2016). https://doi.org/10.1145/2951913.2951926
Thiemann, P., Vasconcelos, V.T.: Label-dependent session types. Proc. ACM Program. Lang. 4(POPL), 67:1–67:29 (2020). https://doi.org/10.1145/3371135
Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP. pp. 161–172. ACM (2011). https://doi.org/10.1145/2003476.2003499
Valiant, L.G.: Decision procedures for families of deterministic pushdown automata. Ph.D. thesis, University of Warwick (1973)
Valiant, L.G., Paterson, M.S.: Deterministic one-counter automata. Journal of Computer and System Sciences 10(3), 340–350 (1975)
Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52–70 (2012). https://doi.org/10.1016/j.ic.2012.05.002
Yoshida, N., Deniélou, P., Bejleri, A., Hu, R.: Parameterised multiparty session types. In: FOSSACS. LNCS, vol. 6014, pp. 128–145. Springer (2010). https://doi.org/10.1007/978-3-642-12032-9_10
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Gay, S.J., Poças, D., Vasconcelos, V.T. (2022). The Different Shades of Infinite Session Types. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)
