Skip to main content
SpringerLink
Log in

Bounded Session Types for Object Oriented Languages

  • Conference paper
Formal Methods for Components and Objects (FMCO 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4709))

Included in the following conference series:

Abstract

Earlier work explored the introduction of session types into object oriented languages. Following the session types literature, two parties would start communicating, provided the types attached to that communication, i.e. the corresponding session types, were dual of each other. Then, the type system was able to ensure soundness, in the sense that two communicating partners were guaranteed to receive/send sequences of values following the order specified by their session types.

In the current paper we improve upon our earlier work in two ways: we extend the type system to support bounded polymorphism, and we make the selection more object-oriented, so that control structures determine how to continue evaluation, depending on the class of the object being sent/received.

Interestingly, although our notion of selection is more powerful than that in earlier work, the ensuing system turned out not to be more complex, except for the notion of duality, which needed to be extended, to correctly deal with bounded polymorphism, and to capture the new notion of selection.

The paper contains an example, informal explanations, a formal description of the operational semantics and of type system, and a proof of subject reduction.

This work was partly funded by FP6-2004-510996 Coordination Action TYPES, by the Information Society Technologies programme of the European Commission, Future and Emerging Technologies under the IST-2005-015905 MOBIUS project and by EPSRC GR/T03208, GR/S55538, GR/T04724 and GR/S68071. This paper reflects only the authors’ views and the Community is not liable for any use that may be made of the information contained therein.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence Assertions for Process Synchronization in Concurrent Communications. Journal of Functional Programming 15(2), 219–248 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bracha, G., Odersky, M., Stoutamire, D., Wadler, P.: Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. In: Chambers, C. (ed.) OOPSLA ’98, pp. 183–200. ACM Press, New York (1998)

    Chapter  Google Scholar 

  3. Bruce, K.B., Schuett, A., van Gent, R., Fiech, A.: PolyTOIL: A Type-safe Polymorphic Object-oriented Language. ACM TOPLAS 25(2), 225–290 (2003)

    Article  Google Scholar 

  4. Canning, P., Cook, W., Hill, W., Olthoff, W., Mitchell, J.C.: F-bounded Polymorphism for Object-Oriented Programming. In: FPCA’89, pp. 273–280. ACM Press, New York (1989)

    Google Scholar 

  5. Carbone, M., Honda, K., Yoshida, N.: A Calculus of Global Interaction Based on Session Types. In: DCM’06. ENTCS, Elsevier, Amsterdam (to appear, 2007)

    Google Scholar 

  6. Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Programming for Web Services. In: De Nicola, R. (ed.) ESOP’07. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)

    Google Scholar 

  7. Cardelli, L., Wegner, P.: On Understanding Types, Data Abstraction, and Polymorphism. Computing Surveys 17(4), 471–522 (1985)

    Article  Google Scholar 

  8. Castagna, G., De Nicola, R., Varacca, D.: Semantic Subtyping for the π-calculus. In: Panangaden, P. (ed.) LICS ’05, pp. 92–101. IEEE Computer Society Press, Los Alamitos (2005)

    Google Scholar 

  9. Castagna, G., Frisch, A.: A Gentle Introduction to Semantic Subtyping. In: Barahona, P., Felty, A. (eds.) PPDP’05, pp. 198–208. ACM Press, New York (2005) (joint ICALP-PPDP keynote talk)

    Google Scholar 

  10. Coppo, M., Dezani-Ciancaglini, M., Yoshida, N.: Asynchronous Session Types and Progress for Object-Oriented Languages. In: Bonsangue, M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 1–31. Springer, Heidelberg (2007)

    Google Scholar 

  11. Corin, R., Denielou, P.-M., Fournet, C., Bhargavan, K., Leifer, J.: Secure Implementations for Typed Session Abstractions. In: CFS’07, IEEE-CS Press, Los Alamitos (to appear, 2007)

    Google Scholar 

  12. Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session Types for Object-Oriented Languages. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 328–352. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. Frisch, A., Castagna, G., Benzaken, V.: Semantic Subtyping. In: Plotkin, G. (ed.) LICS’02, pp. 137–146. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  15. Garralda, P., Compagnoni, A., Dezani-Ciancaglini, M.: BASS: Boxed Ambients with Safe Sessions. In: Maher, M. (ed.) PPDP’06, pp. 61–72. ACM Press, New York (2006)

    Google Scholar 

  16. Gay, S., Hole, M.: Subtyping for Session Types in the Pi-Calculus. Acta Informatica 42(2/3), 191–225 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  17. Gay, S., Vasconcelos, V.T., Ravara, A.: Session Types for Inter-Process Communication. TR 2003–133, Department of Computing, University of Glasgow (2003)

    Google Scholar 

  18. Gay, S.J.: Bounded Polymorphism in Session Types. Mathematical Structures in Computer Science (to appear, 2007)

    Google Scholar 

  19. Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993)

    Google Scholar 

  20. Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Disciplines for Structured Communication-based Programming. In: Hankin, C. (ed.) ESOP 1998 and ETAPS 1998. LNCS, vol. 1381, pp. 22–138. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  21. Honda, K., Yoshida, N., Carbone, M.: Web Services, Mobile Processes and Types. EATCS Bulletin 2, 160–185 (2007)

    Google Scholar 

  22. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a Minimal Core Calculus for Java and GJ. ACM TOPLAS 23(3), 396–450 (2001)

    Article  Google Scholar 

  23. Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Information and Computation, 100(1) (1992)

    Google Scholar 

  24. Mostrous, D., Yoshida, N.: Two session typing systems for higher-order mobile processes. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol. 4583, Springer, Heidelberg (2007)

    Google Scholar 

  25. Odersky, M., Wadler, P.: Pizza into Java: Translating Theory into Practice. In: Felleisen, M. (ed.) POPL’97, pp. 146–159. ACM Press, New York (1997)

    Google Scholar 

  26. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  27. Sparkes, S.: Conversation with Steve Ross-Talbot. ACM Queue 4(2), 14–23 (2006)

    Article  Google Scholar 

  28. 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 

  29. Vallecillo, A., Vasconcelos, V.T., Ravara, A.: Typing the Behavior of Objects and Components using Session Types. In: Brogi, A., Jacquet, J.-M. (eds.) FOCLASA’02. ENTCS, vol. 68(3), pp. 439–456. Elsevier, Amsterdam (2002)

    Google Scholar 

  30. Vasconcelos, V.T., Gay, S., Ravara, A.: Typechecking a Multithreaded Functional Language with Session Types. Theorical Computer Science 368(1-2), 64–87 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  31. Walker, D.: Substructural Type Systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 3–44. MIT Press, Cambridge (2005)

    Google Scholar 

  32. Web Services Choreography Working Group: Web Services Choreography Description Language, http://www.w3.org/2002/ws/chor/

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Torino,  

    Mariangiola Dezani-Ciancaglini & Elena Giachino

  2. Department of Computing, Imperial College London,  

    Sophia Drossopoulou & Nobuko Yoshida

Authors
  1. Mariangiola Dezani-Ciancaglini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Elena Giachino
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sophia Drossopoulou
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Nobuko Yoshida
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Frank S. de Boer Marcello M. Bonsangue Susanne Graf Willem-Paul de Roever

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dezani-Ciancaglini, M., Giachino, E., Drossopoulou, S., Yoshida, N. (2007). Bounded Session Types for Object Oriented Languages. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2006. Lecture Notes in Computer Science, vol 4709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74792-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74792-5_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74791-8

  • Online ISBN: 978-3-540-74792-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation