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.
Work partially supported by the Royal Society, by EU within the FET – Global Computing initiative, project DART IST-2001-33477, and by EPSRC Advanced Fellowship (GR/T03208/01) and EPSRC GR/R33465/02, GR/S55538/01 and GR/T04724/01.
An erratum to this chapter can be found at http://dx.doi.org/10.1007/11580850_20 .
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Ancona, D., Lagorio, G., Zucca, E.: Simplifying Types in a Calculus for Java Exceptions. Technical report, DISI - Università di Genova (2002)
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)
Bonelli, E., Compagnoni, A., Gunter, E.: Typechecking Safe Process Synchronization. In: FGUC 2004, ENTCS (2004)
Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence Assertions for Process Synchronization in Concurrent Communications. To appear in JFP (2005)
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)
Cardelli, L., Gordon, A.D.: Mobile Ambients. Theoretical Computer Science 240(1), 177–213 (2000); Special Issue on Coordination, Le Métayer D.(Ed.)
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/
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Drossopoulou, S.: Advanced Issues in Object Oriented Languages Course Notes, http://www.doc.ic.ac.uk/~scd/Teaching/AdvOO.html
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)
Fahndrich, M., DeLine, R.: Adoption and Focus: Practical Linear Types for Imperative Programming. In: PLDI 2002, pp. 13–24. ACM Press, New York (2002)
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)
Gay, S., Vasconcelos, V.T., Ravara, A.: Session Types for Inter-process Communication. TR 2003–133, Department of Computing, University of Glasgow (March 2003)
Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)
Honda, K.: Composing Processes. In: POPL 1996, pp. 344–357. ACM Press, New York (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. 22–138. Springer, Heidelberg (1998)
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)
Kobayashi, N., Pierce, B., Turner, D.: Linear Types and π-calculus. In: POPL 1996, pp. 358–371. ACM Press, New York (1996)
Sun Microsystems Inc. Java home page, http://www.javasoft.com/
Sun Microsystems Inc. The Java Tutorial: All About Sockets, http://java.sun.com/docs/books/tutorial/networking/sockets/
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Information and Computation 100(1) (1992)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
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)
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)
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)
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)
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)
Web Services Choreography Working Group. Web Services Choreography Description Language, http://www.w3.org/2002/ws/chor/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dezani-Ciancaglini, M., Yoshida, N., Ahern, A., Drossopoulou, S. (2005). A Distributed Object-Oriented Language with Session Types. In: De Nicola, R., Sangiorgi, D. (eds) Trustworthy Global Computing. TGC 2005. Lecture Notes in Computer Science, vol 3705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11580850_16
Download citation
DOI: https://doi.org/10.1007/11580850_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30007-6
Online ISBN: 978-3-540-31483-7
eBook Packages: Computer ScienceComputer Science (R0)