Abstract
A session type is an abstraction of a sequence of heterogeneous values sent over one channel between two communicating processes. Session types have been introduced to guarantee consistency of the exchanged data and, more recently, progress of the session, i.e. the property that once a communication has been established, well-formed programs will never starve at communication points. A relevant feature which influences progress is whether the communication is synchronous or asynchronous. In this paper, we first formulate a typed asynchronous multi-threaded object-oriented language with thread spawning, iterative and higher order sessions. Then we study its progress through a new effect system. As far as we know, ours is the first session type system which assures progress in asynchronous communication.
This work was partly funded by FP6-2004-510996 Coordination Action TYPES, EPSRC GR/T03208, EPSRC GR/S55538, EPSRC GR/T04724, EPSRC GR/S68071, and EU IST–2005–015905 MOBIUS project.
Chapter PDF
Similar content being viewed by others
Keywords
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
Bierman, G., Parkinson, M., Pitts, A.: MJ: An Imperative Core Calculus for Java and Java with Effects. Technical Report 563, Univ. of Cambridge Computer Laboratory (2003)
Bonelli, E., Compagnoni, A., Gunter, E.: Assertions for Process Synchronization in Concurrent Communications. Journal of Functional Programming 15(2), 219–248 (2005)
Carbone, M., Honda, K., Yoshida, N.: A Theoretical Basis of Communication-centered Concurrent Programming. Web Services Choreography Working Group mailing list, to appear as a WS-CDL working report
Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Programming for Web Services. In: ESOP’07. LNCS, Springer, Heidelberg (to appear, 2007)
Dezani-Ciancaglini, M., Drossopoulou, S., Giachino, E., Yoshida, N.: Bounded Session Types for Object-Oriented Languages (2007), http://www.di.unito.it/~dezani/papers/ddgy.pdf
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)
Dezani-Ciancaglini, M., Yoshida, N., Ahern, A., Drossopoulou, S.: A Distributed Object Oriented Language with Session Types. In: Nicola, R.D., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 299–318. Springer, Heidelberg (2005)
Drossopoulou, S.: Advanced Issues in Object Oriented Languages Course Notes. http://www.doc.ic.ac.uk/~scd/Teaching/AdvOO.html
Fähndrich, M., Aiken, M., Hawblitzel, C., Hodson, O., Hunt, G.C., Larus, J.R., Levi, S.: Language Support for Fast and Reliable Message-based Communication in Singularity OS. In: Zwaenepoel, W. (ed.) EuroSys2006, ACM SIGOPS, pp. 177–190. ACM Press, New York (2006)
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)
Gay, S., Hole, M.: Subtyping for Session Types in the Pi-Calculus. Acta Informatica 42(2/3), 191–225 (2005)
Gay, S., Vasconcelos, V.T.: A New Approach to Functional Session Types (2006), http://www.di.fc.ul.pt/~vv/papers/gay.vasconcelos:new-functional-sessions.pdf
Gay, S., Vasconcelos, V.T., Ravara, A.: Session Types for Inter-Process Communication. TR 2003–133, Department of Computing, University of Glasgow (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: Steele, G.L. (ed.) POPL’96, pp. 344–357. ACM Press, New York (1996)
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)
Honda, K., Yoshida, N., Carbone, M.: Web Services, Mobile Processes and Types. EATCS Bulletin (to appear, 2007)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a Minimal Core Calculus for Java and GJ. ACM TOPLAS 23(3), 396–450 (2001)
S. Microsystems Inc. The Java Tutorial: All About Sockets. http://java.sun.com/docs/books/ tutorial/networking/sockets/
S. Microsystems Inc. New IO APIs. http://java.sun.com/j2se/1.4.2/docs/guide/nio/ index.html
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Information and Computation 100(1) (1992)
Neubauer, M., Thiemann, P.: Session Types for Asynchronous Communication. Universität Freiburg (2004)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge, MA (2002)
Sparkes, S.: Conversation with Steve Ross-Talbot. ACM Queue 4(2), 14–23 (2006)
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: Brogi, A., Jacquet, J.-M. (eds.) FOCLASA’02. ENTCS, vol. 68(3), pp. 439–456. Elsevier, Amsterdam (2002)
Vasconcelos, V.T., Gay, S., Ravara, A.: Typechecking a Multithreaded Functional Language with Session Types. Theorical Computer Science 368(1-2), 64–87 (2006)
Web Services Choreography Working Group. Web Services Choreography Description Language. http://www.w3.org/2002/ws/chor/
Yoshida, N., Vasconcelos, V.T.: Language Primitives and Type Disciplines for Structured Communication-based Programming Revisited. In: SecRet’06. ENTCS, Elsevier, Amsterdam (to appear, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Coppo, M., Dezani-Ciancaglini, M., Yoshida, N. (2007). Asynchronous Session Types and Progress for Object Oriented Languages. In: Bonsangue, M.M., Johnsen, E.B. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2007. Lecture Notes in Computer Science, vol 4468. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72952-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-72952-5_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72919-8
Online ISBN: 978-3-540-72952-5
eBook Packages: Computer ScienceComputer Science (R0)