Session types for linear multithreaded functional programming

ABSTRACT

The construction of reliable concurrent and distributed systems is an extremely difficult endeavour. For complex systems, it requires modular development strategies based on precise interface specifications that allow the various modules to interact properly. In this extended abstract we are concerned with message passing systems where partners engage in long and complex interactions, as opposed to, say, remote procedure calls composed of a pair of simple interactions.

Session types allow for the description of continuous series of interactions between several partners. In the simpler case, they detail protocols between two partners; recently the original setting was widened to encompass multiple partners.

In this paper we deal with binary sessions only. Through a running example we visit session types and a functional concurrent language equipped with buffered semantics. Apart from the traditional "well typed programs do not go wrong", the semantics proposed allows for two extra interesting results: the ability to predict the required buffer size, and that of anticipating an output with respect to an input operation.

REFERENCES

• 1: Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. Language support for fast and reliable message-based communication in singularity OS. SIGOPS Oper. Syst. Rev., 40(4):177--190, 2006.
• 2: Simon Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Subsumes Technical Report 2007--251, University of Glasgow, 2008.
• 3: Simon J. Gay and Malcolm J. Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2/3):191--225, 2005.
• 4: Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP'98, volume 1381 of LNCS, pages 22--138. Springer-Verlag, 1998.
• 5: Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. SIGPLAN Not., 43(1):273--284, 2008.
• 6: Dimitris Mostrous and Nobuko Yoshida. Session-based communication optimisation for higher-order mobile processes. In Typed Lambda Calculi and Applications (TLCA'09), LNCS. Springer-Verlag, 2009. To appear.
• 7: Matthias Neubauer and Peter Thiemann. An implementation of session types. In Proceedings of PADL'04, volume 3057 of LNCS, pages 56--70. Springer, 2004a.
• 8: Matthias Neubauer and Peter Thiemann. Session types for asynchronous communication. Unpublished, 2004b.
• 9: Antonio Vallecillo, Vasco T. Vasconcelos, and António Ravara. Typing the behavior of objects and components using session types. Fundamenta Informaticæ, 73(4):583--598, 2006.
• 10: Vasco T. Vasconcelos. 9th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Web Services (SFM 2009), volume 5569 of LNCS, chapter Fundamentals of Session Types, pages 158--186. Springer-Verlag, 2009.
• 11: Vasco T. Vasconcelos, António Ravara, and Simon Gay. Session types for functional multithreading. In CONCUR'04, volume 3170 of LNCS, pages 497--511. Springer-Verlag, 2004.
• 12: Vasco T. Vasconcelos, Simon Gay, and António Ravara. Typechecking a multithreaded functional language with session types. TCS, 368(1-2): 64--87, 2006.
• 13: Philip Wadler. Linear types can change the world. In M. Broy and C.B. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561--581. North-Holland, 1990.
• 14: David Walker. Advanced Topics in Types and Programming Languages, chapter Substructural Type Systems. MIT Press, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

General Terms:
Design, Languages, Theory

Keywords:
concurrency, functional programming, linear type systems, session types