Advertisement

A Distributed Object-Oriented Language with Session Types

  • Mariangiola Dezani-Ciancaglini
  • Nobuko Yoshida
  • Alexander Ahern
  • Sophia Drossopoulou
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)

Abstract

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such as ensuring the correct composition of communication behaviours and guaranteeing deadlock-freedom of their protocols.

This paper proposes the language \(\mathcal{L}_{doos}\), a simple distributed object-oriented language augmented with session communication primitives and types. \(\mathcal{L}_{doos}\) provides a flexible object-oriented programming style for structural interaction protocols by prescribing channel usages within signatures of distributed classes.

We develop a typing system for \(\mathcal{L}_{doos}\) and prove its soundness with respect to the operational semantics. We also show that in a well-typed \(\mathcal{L}_{doos}\) program, there will never be a connection error, a communication error, nor an incorrect completion between server-client interactions. These results demonstrate that a consistent integration of object-oriented language features and session types can statically check the consistent composition of communication protocols.

Keywords

Operational Semantic Minimum Price Method Invocation Session Communication Session 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Ahern, A., Yoshida, N.: Formalising Java RMI with Explicit Code Mobility. In: OOPSLA 2005, the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications. ACM Press, New York (2005) (to appear)Google Scholar
  2. 2.
    Ancona, D., Lagorio, G., Zucca, E.: Simplifying Types in a Calculus for Java Exceptions. Technical report, DISI - Università di Genova (2002)Google Scholar
  3. 3.
    Bierman, G., Parkinson, M., Pitts, A.: MJ: An Imperative Core Calculus for Java and Java with Effects. Technical Report 563, University of Cambridge Computer Laboratory (April 2003)Google Scholar
  4. 4.
    Bonelli, E., Compagnoni, A., Gunter, E.: Typechecking Safe Process Synchronization. In: FGUC 2004, ENTCS (2004)Google Scholar
  5. 5.
    Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence Assertions for Process Synchronization in Concurrent Communications. To appear in JFP (2005)Google Scholar
  6. 6.
    Bracha, G., Odersky, M., Stoutamire, D., Wadler, P.: Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. In: OOPSLA 1998, pp. 183–200. ACM Press, New York (1998)CrossRefGoogle Scholar
  7. 7.
    Cardelli, L., Gordon, A.D.: Mobile Ambients. Theoretical Computer Science 240(1), 177–213 (2000); Special Issue on Coordination, Le Métayer D.(Ed.)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Dezani-Ciancaglini, M., Yoshida, N., Ahern, A., Drossopoulou, S.: A Distributed Object-Oriented Language with Session Types. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 299–318. Springer, Heidelberg (2005), http://www.cs.unibo.it/~sangio/TGC05/ CrossRefGoogle Scholar
  9. 9.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  10. 10.
    Drossopoulou, S.: Advanced Issues in Object Oriented Languages Course Notes, http://www.doc.ic.ac.uk/~scd/Teaching/AdvOO.html
  11. 11.
    Drossopoulou, S., Lagorio, G., Eisenbach, S.: Flexible Models for Dynamic Linking. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 38–53. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Fahndrich, M., DeLine, R.: Adoption and Focus: Practical Linear Types for Imperative Programming. In: PLDI 2002, pp. 13–24. ACM Press, New York (2002)CrossRefGoogle Scholar
  13. 13.
    Gay, S., Hole, M.: Types and Subtypes for Client-Server Interactions. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 74–90. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  14. 14.
    Gay, S., Vasconcelos, V.T., Ravara, A.: Session Types for Inter-process Communication. TR 2003–133, Department of Computing, University of Glasgow (March 2003)Google Scholar
  15. 15.
    Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)Google Scholar
  16. 16.
    Honda, K.: Composing Processes. In: POPL 1996, pp. 344–357. ACM Press, New York (1996)CrossRefGoogle Scholar
  17. 17.
    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. 22–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a Minimal Core Calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23(3), 396–450 (2001)CrossRefGoogle Scholar
  19. 19.
    Kobayashi, N., Pierce, B., Turner, D.: Linear Types and π-calculus. In: POPL 1996, pp. 358–371. ACM Press, New York (1996)CrossRefGoogle Scholar
  20. 20.
    Sun Microsystems Inc. Java home page, http://www.javasoft.com/
  21. 21.
    Sun Microsystems Inc. The Java Tutorial: All About Sockets, http://java.sun.com/docs/books/tutorial/networking/sockets/
  22. 22.
    Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Information and Computation 100(1) (1992)Google Scholar
  23. 23.
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)Google Scholar
  24. 24.
    Pierce, B.C., Sangiorgi, D.: Typing and Subtyping for Mobile Processes. Logic in Computer Science (1993). Full version in bgroup Mathematical Structures in Computer Science egroup 6(5) (1996)Google Scholar
  25. 25.
    Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)Google Scholar
  26. 26.
    Vallecillo, A., Vasconcelos, V.T., Ravara, A.: Typing the Behavior of Objects and Components using Session Types. In: Foclasa 2002. ENTCS, vol. 68(3). Elsevier, Amsterdam (2002)Google Scholar
  27. 27.
    Vasconcelos, V.T., Ravara, A., Gay, S.: Session Types for Functional Multithreading. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 497–511. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  28. 28.
    Vitek, J., Castagna, G.: Seal: A Framework for Secure Mobile Computations. In: Bal, H.E., Cardelli, L., Belkhouche, B. (eds.) ICCL-WS 1998. LNCS, vol. 1686, pp. 47–77. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  29. 29.
    Web Services Choreography Working Group. Web Services Choreography Description Language, http://www.w3.org/2002/ws/chor/

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Mariangiola Dezani-Ciancaglini
    • 1
  • Nobuko Yoshida
    • 2
  • Alexander Ahern
    • 2
  • Sophia Drossopoulou
    • 2
  1. 1.Dipartimento di InformaticaUniversità di TorinoItaly
  2. 2.Department of ComputingImperial College LondonUK

Personalised recommendations