Abstract
Session types denote message protocols between concurrent processes, allowing a type-safe expression of inter-process communication. Although previous work demonstrate a well-defined notion of subtyping where processes have different perceptions of the protocol, these formulations were limited to linear session types where each channel of communication has a unique provider and client. In this paper, we extend subtyping to shared session types where channels can now have multiple clients instead of a single client. We demonstrate that this generalization can statically capture protocol requirements that span multiple phases of interactions of a client with a shared service provider, something not possible in prior proposals. Moreover, the phases are manifest in the type of the client.
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
Notes
- 1.
We do not consider termination to more easily align with later examples.
- 2.
The currently unnecessary unary choice will be useful later.
References
Acay, C., Pfenning, F.: Intersections and unions of session types. In: Kobayashi, N. (ed.) 8th Workshop on Intersection Types and Related Systems (ITRS 2016), EPTCS 242, Porto, Portugal, pp. 4–19, June 2016
Balzer, S., Pfenning, F.: Manifest sharing with session types. In: International Conference on Functional Programming (ICFP), pp. 37:1–37:29. ACM, September 2017. Extended version available as Technical Report CMU-CS-17-106R, June 2017
Balzer, S., Toninho, B., Pfenning, F.: Manifest deadlock-freedom for shared session types. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 611–639. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_22
Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15375-4_16
Cervesato, I., Scedrov, A.: Relating state-based and process-based concurrency through linear logic. Inf. Comput. 207(10), 1044–1077 (2009)
Chen, T.c., Dezani-Ciancaglini, M., Scalas, A., Yoshida, N.: On the preciseness of subtyping in session types. Log. Methods Comput. Sci. 13(2) (2017). https://doi.org/10.23638/LMCS-13(2:12)2017
Chen, T.C., Dezani-Ciancaglini, M., Yoshida, N.: On the preciseness of subtyping in session types. In: Proceedings of the Conference on Principles and Practice of Declarative Programming (PPDP 2014), Canterbury, UK. ACM, September 2014
Crary, K., Harper, R., Puri, S.: What is a recursive module? In: In SIGPLAN Conference on Programming Language Design and Implementation, pp. 50–63. ACM Press (1999)
Das, A., Balzer, S., Hoffmann, J., Pfenning, F., Santurkar, I.: Resource-aware session types for digital contracts. In: Küsters, R., Naumann, D. (eds.) 34th Computer Security Foundations Symposium (CSF 2021), Dubrovnik, Croatia. IEEE (June 2021, to appear)
Das, A., Pfenning, F.: Session types with arithmetic refinements. In: Konnov, I., Kovács, L. (eds.) 31st International Conference on Concurrency Theory (CONCUR 2020), LIPIcs, Vienna, Austria, vol. 171, pp. 13:1–13:18, September 2020
Gay, S.J., Hole, M.: Subtyping for session types in the \(\pi \)-calculus. Acta Informatica 42(2–3), 191–225 (2005)
Ghilezan, S., Jakšić, S., Pantović, J., Scalas, A., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. J. Log. Algebr. 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 (2020)
Griffith, D.: Polarized substructural session types. Ph.D. thesis, University of Illinois at Urbana-Champaign (2015, in preparation)
Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (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: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053567
Pfenning, F., Griffith, D.: Polarized substructural session types. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 3–22. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46678-0_1
Pruiksma, K., Pfenning, F.: A message-passing interpretation of adjoint logic. In: Martins, F., Orchard, D. (eds.) Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES), EPTCS 291, Prague, Czech Republic, pp. 60–79, April 2019
Sano, C.: On Session Typed Contracts for Imperative Languages. Masters thesis, Carnegie Mellon University, December 2019. Available as Technical Report CMU-CS-19-133, December 2019
Sano, C., Balzer, S., Pfenning, F.: Manifestly phased communication via shared session types. CoRR abs/2101.06249 (2021). https://arxiv.org/abs/2101.06249
Toninho, B.: A logical foundation for session-based concurrent computation. Ph.D. thesis, Carnegie Mellon University and Universidade Nova de Lisboa, May 2015. Available as Technical Report CMU-CS-15-109
Wadler, P.: Propositions as sessions. In: Proceedings of the 17th International Conference on Functional Programming (ICFP 2012), Copenhagen, Denmark, pp. 273–286. ACM Press, September 2012
Acknowledgements
We would like to thank the anonymous reviewers for feedback on the initially submitted version of this paper.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 IFIP International Federation for Information Processing
About this paper
Cite this paper
Sano, C., Balzer, S., Pfenning, F. (2021). Manifestly Phased Communication via Shared Session Types. 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_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-78142-2_2
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)