Abstract
Binary session types can be used to describe communication protocols, and to ensure a variety of properties, e.g. deadlock freedom, liveness, or secure information flow. Session type systems are often formulated for variants of the \(\pi \)-calculus, and for each such system, the central properties such as session fidelity must be re-established.
The framework of psi-calculi introduced by Bengtson et al. makes it possible to give a general account of variants of the pi-calculus. We use this framework to describe a generic session type system for variants of the \(\pi \)-calculus. In this generic system, standard properties, including fidelity, hold at the level of the framework and are then guaranteed to hold when the generic system is instantiated.
We show that our system can capture existing systems including the session type system due to Gay and Hole, a type system for progress due to Vieira and Vasconcelos and a refinement type system due to Baltazar et al. The standard fidelity property is proved at the level of the generic system, and automatically hold when the system is instantiated.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Baltazar, P., Mostrous, D., Vasconcelos, V.T.: Linearly refined session types. In: LINEARITY, pp. 38–49 (2012)
Bengtson, J., Johansson, M., Parrow, J., Victor, B.: psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods Comput. Sci. 7(1) (2011)
Bernardi, G., Hennessy, M.: Using higher-order contracts to model session types (Extended Abstract). In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 387–401. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44584-6_27
Bernardi, G., Dardha, O., Gay, S.J., Kouzapas, D.: On duality relations for session types. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 51–66. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45917-1_4
Borgström, J., Gutkovas, R., Parrow, J., Victor, B., Pohjola, J.Å.: A sorted semantic framework for applied process calculi (Extended Abstract). In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 103–118. Springer, Heidelberg (2014). doi:10.1007/978-3-319-05119-2_7
Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: PPDP, pp. 219–230. ACM (2009)
Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5), 19: 1–19: 61 (2009)
Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming, PPDP 2012, pp. 139–150. ACM, New York (2012)
Dezani-Ciancaglini, M., de’Liguoro, U., Yoshida, N.: On progress for structured communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 257–275. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78663-4_18
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst., 29(5) (2007)
Gabbay, M.J., Mathijssen, A.: Nominal (universal) algebra: equational logic with names and binding. J. Log. Comput. 19(6), 1455–1508 (2009)
Gay, S.J.: Bounded polymorphism in session types. Math. Struct. Comput. Sci. 18(5), 895–930 (2008)
Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2–3), 191–225 (2005)
Giunti, M., Vasconcelos, V.T.: A linear account of session types in the pi calculus. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 432–446. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15375-4_30
Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. J. Comput. Secur. 11(4), 451–519 (2003)
Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993). doi:10.1007/3-540-57208-2_35
Honda, K.: Composing processes. In: POPL, pp. 344–357 (1996)
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). doi:10.1007/BFb0053567
Hüttel, H.: Typed \(\pi \)-calculi. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 265–279. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23217-6_18
Hüttel, H.: Types for resources in \(\psi \)-calculi. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 83–102. Springer, Heidelberg (2014). doi:10.1007/978-3-319-05119-2_6
Igarashi, A., Kobayashi, N.: A generic type system for the Pi-calculus. Theoret. Comput. Sci. 311(1–3), 121–163 (2004)
Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006). doi:10.1007/11817949_16
König, B.: Analysing input/output-capabilities of mobile processes with a generic type system. J. Logic Algebraic Program. 63(1), 35–58 (2005)
Torres Vieira, H., Thudichum Vasconcelos, V.: Typing progress in communication-centred systems. In: Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 236–250. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38493-6_17
Acknowledgements
The author would like to thank Johannes Borgström and Björn Victor for useful comments and suggestions. The work was supported by the COST Action IC1021 BETTY.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Hüttel, H. (2016). Binary Session Types for Psi-Calculi. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-47958-3_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47957-6
Online ISBN: 978-3-319-47958-3
eBook Packages: Computer ScienceComputer Science (R0)