Article

Session types for object-oriented languages

Authors:

Mariangiola Dezani-Ciancaglini,

Dimitris Mostrous,

Nobuko Yoshida,

Sophia DrossopoulouAuthors Info & Claims

ECOOP'06: Proceedings of the 20th European conference on Object-Oriented Programming

Pages 328 - 352

https://doi.org/10.1007/11785477_20

Published: 03 July 2006 Publication History

Abstract

A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other. Session types characterise such sessions in terms of the types of values communicated and the shape of protocols, and have been developed for the π-calculus, CORBA interfaces, and functional languages. We study the incorporation of session types into object-oriented languages through Moose, a multi-threaded language with session types, thread spawning, iterative and higher-order sessions. Our design aims to consistently integrate the object-oriented programming style and sessions, and to be able to treat various case studies from the literature. We describe the design of Moose, its syntax, operational semantics and type system, and develop a type inference system. After proving subject reduction, we establish the progress property: once a communication has been established, well-typed programs will never starve at communication points.

References

[1]

A full version of this paper. http://www.doc.ic.ac.uk/~dm04.

[2]

Personal communication by e-mails between the authors of {6, 7, 13, 15, 18, 20, 26, 27, 29}.

[3]

Conversation with Steve Ross-Talbot. ACM Queue, 4(2), 2006.

Digital Library

[4]

A. Ahern and N. Yoshida. Formalising Java RMI with Explicit Code Mobility. In OOPSLA '05, pages 403-422. ACM Press, 2005.

Digital Library

[5]

G. Bierman, M. Parkinson, and A. Pitts. MJ: An Imperative Core Calculus for Java and Java with Effects. Technical Report 563, Univ. of Cambridge Computer Laboratory, 2003.

[6]

E. Bonelli, A. Compagnoni, and E. Gunter. Correspondence Assertions for Process Synchronization in Concurrent Communications. J. of Funct. Progr., 15(2):219-248, 2005.

Digital Library

[7]

E. Bonelli, A. Compagnoni, and E. Gunter. Typechecking Safe Process Synchronization. In FGUC 2004, volume 138 of ENTCS, pages 3-22. Elsevier, 2005.

Digital Library

[8]

M. Carbone, K. Honda, and N. Yoshida. A Theoretical Basis of Communication-centered Concurrent Programming. Web Services Choreography Working Group mailing list, to appear as a WS-CDL working report.

[9]

R. DeLine and M. Fahndrich. Enforcing High-Level Protocols in Low-Level Software. In PLDI '01, volume 36(5) of SIGPLAN Notices, pages 59-69. ACM Press, 2001.

Digital Library

[10]

M. Dezani-Ciancaglini, N. Yoshida, A. Ahern, and S. Drossopoulou. A Distributed Object Oriented Language with Session Types. In TGC'05, volume 3705 of LNCS, pages 299-318. Springer-Verlag, 2005.

Digital Library

[11]

S. Drossopoulou. Advanced issues in object oriented languages course notes. http://www.doc.ic.ac.uk/~scd/Teaching/AdvOO.html.

[12]

M. Fahndrich and R. DeLine. Adoption and focus: practical linear types for imperative programming. In PLDI '02, pages 13-24. ACM Press, 2002.

Digital Library

[13]

S. Gay and M. Hole. Types and Subtypes for Client-Server Interactions. In ESOP'99, volume 1576 of LNCS, pages 74-90. Springer-Verlag, 1999.

Digital Library

[14]

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

Digital Library

[15]

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

[16]

A. D. Gordon and A. Jeffrey. Typing Correspondence Assertions for Communication Protocols. In MFPS'01, volume 45 of ENTCS, pages 379-409. Elsevier, 2001.

[17]

M. Hole and S. J. Gay. Bounded Polymorphism in Session Types. Technical Report TR- 2003-132, Department of Computing Science, University of Glasgow, 2003.

[18]

K. Honda. Types for Dyadic Interaction. In CONCUR'93, volume 715 of LNCS, pages 509-523. Springer-Verlag, 1993.

Digital Library

[19]

K. Honda. Composing Processes. In POPL'96, pages 344-357. ACM Press, 1996.

Digital Library

[20]

K. Honda, V. T. Vasconcelos, and M. Kubo. Language Primitives and Type Disciplines for Structured Communication-based Programming. In ESOP'98, volume 1381 of LNCS, pages 22-138. Springer-Verlag, 1998.

Digital Library

[21]

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

Digital Library

[22]

N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the Pi-Calculus. ACM TOPLAS, 21(5):914-947, Sept. 1999.

Digital Library

[23]

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

Digital Library

[24]

D. Mostrous. Moose: a Minimal Object Oriented Language with Session Types. Master's thesis, Imperial College London, 2005.

[25]

B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

Digital Library

[26]

K. Takeuchi, K. Honda, and M. Kubo. An Interaction-based Language and its Typing System. In PARLE'94, volume 817 of LNCS, pages 398-413. Springer-Verlag, 1994.

Digital Library

[27]

A. Vallecillo, V. T. Vasconcelos, and A. Ravara. Typing the Behavior of Objects and Components using Session Types. In FOCLASA'02, volume 68(3) of ENTCS. Elsevier, 2002.

[28]

V. Vasconcelos. Typed Concurrent Objects. In ECOOP'94, volume 821 of LNCS, pages 100-117. Springer-Verlag, 1994.

Digital Library

[29]

V. T. Vasconcelos, A. Ravara, and S. Gay. Session Types for Functional Multithreading. In CONCUR'04, volume 3170 of LNCS, pages 497-511. Springer-Verlag, 2004.

[30]

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

Cited By

de Ferro CCogumbreiro TMartins F(2023)Shelley: A Framework for Model Checking Call Ordering on Hierarchical SystemsCoordination Models and Languages10.1007/978-3-031-35361-1_5(93-114)Online publication date: 19-Jun-2023
https://dl.acm.org/doi/10.1007/978-3-031-35361-1_5
Jacobs JBalzer SKrebbers R(2022)Multiparty GV: functional multiparty session types with certified deadlock freedomProceedings of the ACM on Programming Languages10.1145/35476386:ICFP(466-495)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547638
Jacobs JBalzer SKrebbers R(2022)Connectivity graphs: a method for proving deadlock freedom based on separation logicProceedings of the ACM on Programming Languages10.1145/34986626:POPL(1-33)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498662
Show More Cited By

Recommendations

Modular session types for distributed object-oriented programming
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1)...
Modular session types for distributed object-oriented programming
POPL '10

Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1)...
Bounded session types for object oriented languages
FMCO'06: Proceedings of the 5th international conference on Formal methods for components and objects

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ECOOP'06: Proceedings of the 20th European conference on Object-Oriented Programming

July 2006

525 pages

ISBN:3540357262

Editor:
Dave Thomas
Bedarra Research Lab., 1 Stafford Road, Suite 421, Ottawa, Ontario, Canada

Sponsors

ILOG
Google Inc.
Sun Microsystems
Microsoft Research: Microsoft Research
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 03 July 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

53
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

de Ferro CCogumbreiro TMartins F(2023)Shelley: A Framework for Model Checking Call Ordering on Hierarchical SystemsCoordination Models and Languages10.1007/978-3-031-35361-1_5(93-114)Online publication date: 19-Jun-2023
https://dl.acm.org/doi/10.1007/978-3-031-35361-1_5
Jacobs JBalzer SKrebbers R(2022)Multiparty GV: functional multiparty session types with certified deadlock freedomProceedings of the ACM on Programming Languages10.1145/35476386:ICFP(466-495)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547638
Jacobs JBalzer SKrebbers R(2022)Connectivity graphs: a method for proving deadlock freedom based on separation logicProceedings of the ACM on Programming Languages10.1145/34986626:POPL(1-33)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498662
Jakobsen MRavier ADardha O(2021)Papaya: Global Typestate Analysis of Aliased ObjectsProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479414(1-13)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3479394.3479414
Kokke WDardha OHage J(2021)Deadlock-free session types in linear HaskellProceedings of the 14th ACM SIGPLAN International Symposium on Haskell10.1145/3471874.3472979(1-13)Online publication date: 18-Aug-2021
https://dl.acm.org/doi/10.1145/3471874.3472979
Godoy JGaleotti JGarbervetsky DUchitel S(2021)Enabledness-based Testing of Object ProtocolsACM Transactions on Software Engineering and Methodology10.1145/341515330:2(1-36)Online publication date: 3-Jan-2021
https://dl.acm.org/doi/10.1145/3415153
Derakhshan FBalzer SJia LGorla D(2021)Session logical relations for noninterferenceProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470654(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470654
van Glabbeek RHöfner PHorne RGorla D(2021)Assuming just enough fairness to make session types complete for lock-freedomProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470531(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470531
Kokke WDardha O(2021)Prioritise the Best VariationFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-78089-0_6(100-119)Online publication date: 14-Jun-2021
https://dl.acm.org/doi/10.1007/978-3-030-78089-0_6
Bagherzadeh MRajan HDe Koster JBergenti F(2017)Order types: static reasoning about message races in asynchronous message passing concurrencyProceedings of the 7th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control10.1145/3141834.3141837(21-30)Online publication date: 23-Oct-2017
https://dl.acm.org/doi/10.1145/3141834.3141837
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents