Advertisement

Type-Based Analysis for Session Inference (Extended Abstract)

  • Carlo SpaccasassiEmail author
  • Vasileios Koutavas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9688)

Abstract

We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type system from the typing of sessions. Without using linearity, our system guarantees communication safety and partial lock freedom. It also supports provably complete session inference for finite sessions with no programmer annotations. We exhibit the usefulness of our system with interesting examples, including one which is not typable in substructural type systems.

Keywords

Operational Semantic Type Schema Inference Algorithm Type Inference Communication Safety 
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.

References

  1. 1.
    Amtoft, T., Nielson, H.R., Nielson, F.: Type and Effect Systems - Behaviours for Concurrency. Imperial College Press, London (1999)CrossRefzbMATHGoogle Scholar
  2. 2.
    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
  3. 3.
    Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: PPDP, pp. 219–230. ACM (2009)Google Scholar
  4. 4.
    Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2–3), 191–225 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Gay, S., Vasconcelos, V.: Linear type theory for asynchronous session types. J. Funct. Prog. 20(01), 19–50 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)Google Scholar
  7. 7.
    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
  8. 8.
    Hüttel, H., Lanese, I., Vasconcelos, V., Caires, L., Carbone, M., Deniélou, P., Padovani, L., Ravara, A., Tuosto, E., Vieira, H., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comp. Surv. (To appear)Google Scholar
  9. 9.
    Igarashi, A., Kobayashi, N.: Type reconstruction for linear \(\pi \)-calculus with I/O subtyping. Inf. Comput. 161(1), 1–44 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Mezzina, L.G.: How to infer finite session types in a calculus of services and sessions. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 216–231. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Padovani, L.: Type reconstruction for the linear \(\pi \)-calculus with composite regular types. Logical Methods Comput. Sci. 11(4) (2015)Google Scholar
  12. 12.
    Palsberg, J.: Type-based analysis and applications. In: PASTE, pp. 20–27. ACM (2001)Google Scholar
  13. 13.
    Pucella, R., Tov, J.A.: Haskell session types with (almost) no class. In: Haskell Symposium, pp. 25–36. ACM (2008)Google Scholar
  14. 14.
    Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, CMU (1991)Google Scholar
  15. 15.
    Tofte, M., Talpin, J.: Implementation of the typed call-by-value lambda-calculus using a stack of regions. In: POPL, pp. 188–201. ACM (1994)Google Scholar
  16. 16.
    Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: a monadic integration. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 350–369. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  17. 17.
    Tov, J.: Practical programming with substructural types. Ph.D. thesis, Northeastern University (2012)Google Scholar
  18. 18.
    Vasconcelos, V., Gay, S., Ravara, A.: Type checking a multithreaded functional language with session types. Theor. Computer Sci. 368(1–2), 64–87 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Wadler, P.: Propositions as sessions. In: ICFP, pp. 273–286. ACM (2012)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2016

Authors and Affiliations

  1. 1.Trinity College DublinDublinIreland

Personalised recommendations