The Challenge of Typed Expressiveness in Concurrency

  • Jorge A. PérezEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9688)


By classifying behaviors (rather than data values), behavioral types abstract structured protocols and enforce disciplined message-passing programs. Many different behavioral type theories have been proposed: they offer a rich landscape of models in which types delineate concurrency and communication. Unfortunately, studies on formal relations between these theories are incipient. This paper argues that clarifying the relative expressiveness of these type systems is a pressing challenge for formal techniques in distributed systems. We overview works that address this issue and discuss promising research avenues.


Type System Behavioral Type Type Soundness Session Type Global Type 
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.



I would like to thank Ilaria Castellani, Ornela Dardha, Mariangiola Dezani-Ciancaglini, Dimitrios Kouzapas, Hugo A. López, and Camilo Rueda for their useful feedback on previous drafts of this paper.


  1. 1.
    Flow: A Static Type Checker for JavaScript.
  2. 2.
    The Erlang Programming Language.
  3. 3.
    The Go Programming Language.
  4. 4.
    The Rust Programming Language.
  5. 5.
    Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: mobile processes, nominal data, and logic. In: Proceedings of LICS 2009, pp. 39–48. IEEE Computer Society (2009).
  6. 6.
    Busi, N., Gabbrielli, M., Zavattaro, G.: On the expressive power of recursion, replication and iteration in process calculi. Math. Struc. Comp. Sci. 19(6), 1191–1222 (2009). MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Caires, L., Pérez, J.A.: A typeful characterization of multiparty structured conversations based on binary sessions. CoRR abs/1407.4242 (2014).
  8. 8.
    Caires, L., Pérez, J.A.: Multiparty session types within a canonical binary theory, and beyond. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 75–85. Springer, Heidelberg (2016)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    Cano, M., Rueda, C., López, H.A., Pérez, J.A.: Declarative interpretations of session-based concurrency. In: Proceedings of PPDP 2015, pp. 67–78. ACM (2015).
  11. 11.
    Carbone, M., Dardha, O., Montesi, F.: Progress as compositional lock-freedom. In: Kühn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 49–64. Springer, Heidelberg (2014). CrossRefGoogle Scholar
  12. 12.
    Carbone, M., Debois, S.: A graphical approach to progress for structured communication in web services. In: Proceedings of ICE 2010. EPTCS, vol. 38, pp. 13–27 (2010).
  13. 13.
    Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Proceedings of POPL 2013, pp. 263–274. ACM (2013).
  14. 14.
    Carbone, M., Montesi, F., Schürmann, C., Yoshida, N.: Multiparty session types as coherence proofs. In: Proceedings of CONCUR 2015. LIPIcs, vol. 42, pp. 412–426 (2015).
  15. 15.
    Cruz-Filipe, L., Montesi, F.: Choreographies, computationally. CoRR abs/1510.03271 (2015).
  16. 16.
    Dardha, O.: Recursive session types revisited. In: Proceedings of BEAT 2014. EPTCS, vol. 162, pp. 27–34 (2014).
  17. 17.
    Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: Proceedings of PPDP 2012, pp. 139–150. ACM (2012).
  18. 18.
    Dardha, O., Pérez, J.A.: Comparing deadlock-free session typed processes. In: Proceedings of EXPRESS/SOS. EPTCS, vol. 190, pp. 1–15 (2015).
  19. 19.
    Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  20. 20.
    Demangeon, R., Yoshida, N.: On the expressiveness of multiparty sessions. In: Proceedings of FSTTCS 2015. LIPIcs, vol. 45, pp. 560–574. Schloss Dagstuhl (2015).
  21. 21.
    Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Inf. Comput. 204(7), 1045–1082 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012). CrossRefGoogle Scholar
  23. 23.
    Deniélou, P.-M., Yoshida, N.: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 174–186. Springer, Heidelberg (2013). Google Scholar
  24. 24.
    Dezani-Ciancaglini, M., de’Liguoro, U.: Sessions and session types: an overview. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol. 6194, pp. 1–28. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  25. 25.
    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). CrossRefGoogle Scholar
  26. 26.
    Fossati, L., Hu, R., Yoshida, N.: Multiparty session nets. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 112–127. Springer, Heidelberg (2014). Google Scholar
  27. 27.
    Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42, 191–225 (2005). MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Gay, S.J., Gesbert, N., Ravara, A.: Session types as generic process types. In: Proceedings of EXPRESS 2014 and SOS 2014. EPTCS, vol. 160, pp. 94–110 (2014).
  29. 29.
    Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010). MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010). MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    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)CrossRefGoogle Scholar
  32. 32.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, pp. 273–284. ACM (2008)Google Scholar
  33. 33.
    Hüttel, H.: Typed \(\psi \)-calculi. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 265–279. Springer, Heidelberg (2011). CrossRefGoogle Scholar
  34. 34.
    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). CrossRefGoogle Scholar
  35. 35.
    Huttel, H., Lanese, I., Vasconcelos, V., Caires, L., Carbone, M., Deniélou, P.M., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. (2016, to appear)Google Scholar
  36. 36.
    Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theor. Comput. Sci. 311(1–3), 121–163 (2004).–6 MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    Kobayashi, N.: A type system for lock-free processes. Inf. Comput. 177(2), 122–159 (2002). MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Kobayashi, N.: Type systems for concurrent programs. In: Aichernig, B.K. (ed.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 439–453. Springer, Heidelberg (2003). CrossRefGoogle Scholar
  39. 39.
    Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. In: POPL, pp. 358–371 (1996)Google Scholar
  40. 40.
    Kouzapas, D., Pérez, J.A., Yoshida, N.: On the relative expressiveness of higher-order session processes. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 446–475. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49498-1_18 CrossRefGoogle Scholar
  41. 41.
    Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: Proceedings of POPL 2015, pp. 221–232. ACM (2015).
  42. 42.
    López, H.A., Olarte, C., Pérez, J.A.: Towards a unified framework for declarative structured communications. In: Proceedings of PLACES 2009. EPTCS, vol. 17, pp. 1–15 (2009).
  43. 43.
    Milner, R.: The Polyadic pi-Calculus: A Tutorial. Technical report, ECS-LFCS-91-180 (1991)Google Scholar
  44. 44.
    Milner, R.: Functions as processes. Math. Struc. Comp. Sci. 2(2), 119–141 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  45. 45.
    Nestmann, U.: Welcome to the jungle: a subjective guide to mobile process calculi. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 52–63. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  46. 46.
    Orchard, D.A., Yoshida, N.: Effects as sessions, sessions as effects. In: Proceedings of POPL 2016, pp. 568–581. ACM (2016).
  47. 47.
    Padovani, L.: Session types = intersection types + union types. In: Proceedings of ITRS 2010. EPTCS, vol. 45, pp. 71–89 (2010).
  48. 48.
    Palamidessi, C.: Comparing the expressive power of the synchronous and asynchronous pi-calculi. Math. Struct. Comput. Sci. 13(5), 685–719 (2003). MathSciNetCrossRefGoogle Scholar
  49. 49.
    Parrow, J.: Expressiveness of process algebras. In: ENTCS, vol. 209, pp. 173–186 (2008).
  50. 50.
    Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. Ph.D. thesis CST-99-93, University of Edinburgh (1992)Google Scholar
  51. 51.
    Villard, J.: Heaps and Hops. Ph.D. thesis, École Normale Supérieure de Cachan, February 2011Google Scholar
  52. 52.
    Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2–3), 384–418 (2014). MathSciNetCrossRefzbMATHGoogle Scholar
  53. 53.
    Yoshida, N.: Graph types for monadic mobile processes. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180, pp. 371–386. Springer, Heidelberg (1996). CrossRefGoogle Scholar
  54. 54.
    Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the pi -calculus. Inf. Comput. 191(2), 145–202 (2004)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2016

Authors and Affiliations

  1. 1.University of GroningenGroningenThe Netherlands

Personalised recommendations