Abstract
Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the behaviours accepted. The global types presented in this paper improve the state-of-the-art by extending the set of typeable asynchronous sessions and preserving decidability of type checking together with the key properties of Subject Reduction, Session Fidelity and Progress.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85361-9_33
Bianchini, R., Dagnino, F.: Asynchronous-global-types-implementation. https://github.com/RiccardoBianc/Asynchronous-global-types-implementation
Bianchini, R., Dagnino, F.: Asynchronous global types in co-logic programming. In: Damiani, F., Dardha, O. (eds.) COORDINATION 2021. LNCS, vol. 12717, pp. 134–146. Springer, Cham (2021)
Bravetti, M., Carbone, M., Lange, J., Yoshida, N., Zavattaro, G.: A sound algorithm for asynchronous session subtyping. In: Fokkink, W.J., van Glabbeek, R. (eds.) CONCUR. LIPIcs, vol. 140, pp. 38:1–38:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.CONCUR.2019.38
Bravetti, M., Carbone, M., Zavattaro, G.: Undecidability of asynchronous session subtyping. Inf. Comput. 256, 300–320 (2017). https://doi.org/10.1016/j.ic.2017.07.010
Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theoret. Comput. Sci. 722, 19–51 (2018). https://doi.org/10.1016/j.tcs.2018.02.010
Castellani, I., Dezani-Ciancaglini, M., Giannini, P.: Reversible sessions with flexible choices. Acta Informatica, 553–583 (2019). https://doi.org/10.1007/s00236-019-00332-y
Castellani, I., Dezani-Ciancaglini, M., Giannini, P.: Global types and event structure semantics for asynchronous multiparty sessions. CoRR abs/2102.00865 (2021). https://arxiv.org/abs/2102.00865
Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci. 26(2), 238–302 (2016). https://doi.org/10.1017/S0960129514000188
Courcelle, B.: Fundamental properties of infinite trees. Theoret. Comput. Sci. 25, 95–169 (1983). https://doi.org/10.1016/0304-3975(83)90059-2
Demangeon, R., Honda, K.: Nested protocols in session types. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 272–286. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_20
Deniélou, P.M., Yoshida, N.: Dynamic multirole session types. In: Thomas Ball, M.S. (ed.) POPL, pp. 435–446. ACM Press (2011). https://doi.org/10.1145/1926385.1926435
Dezani-Ciancaglini, M., Ghilezan, S., Jaksic, S., Pantovic, J., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. In: Gay, S., Alglave, J. (eds.) PLACES. EPTCS, vol. 203, pp. 29–44. Open Publishing Association (2016). https://doi.org/10.4204/EPTCS.203.3
Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2/3), 191–225 (2005). https://doi.org/10.1007/s00236-005-0177-z
Ghilezan, S., Jaksic, S., Pantovic, J., Scalas, A., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. J. Logic Algeb. Methods Program. 104, 127–173 (2019). https://doi.org/10.1016/j.jlamp.2018.12.002
Ghilezan, S., Pantović, J., Prokić, I., Scalas, A., Yoshida, N.: Precise subtyping for asynchronous multiparty sessions. Proc. ACM Program. Lang. 5(POPL), 1–28 (2021). https://doi.org/10.1145/3434297
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 273–284. ACM Press (2008). https://doi.org/10.1145/1328897.1328472
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1–9:67 (2016). https://doi.org/10.1145/2827695
Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 441–457. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_26
Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994). https://doi.org/10.1145/197320.197383
Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_23
Severi, P., Dezani-Ciancaglini, M.: Observational equivalence for multiparty sessions. Fundamenta Informaticae 167, 267–305 (2019). https://doi.org/10.1007/s00236-019-00332-y
Acknowledgment
We are grateful to Ilaria Castellani and Elena Zucca for enlightening discussions on the subject of this paper. We thank Elena Zucca also for her careful reading of the paper. Her suggestions led to many improvements. Last but not least we are indebted to the anonymous referees for their constructive remarks.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 IFIP International Federation for Information Processing
About this paper
Cite this paper
Dagnino, F., Giannini, P., Dezani-Ciancaglini, M. (2021). Deconfined Global Types for Asynchronous Sessions. In: Damiani, F., Dardha, O. (eds) Coordination Models and Languages. COORDINATION 2021. Lecture Notes in Computer Science(), vol 12717. Springer, Cham. https://doi.org/10.1007/978-3-030-78142-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-78142-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-78141-5
Online ISBN: 978-3-030-78142-2
eBook Packages: Computer ScienceComputer Science (R0)