Hostname: page-component-8448b6f56d-m8qmq Total loading time: 0 Render date: 2024-04-23T10:41:57.628Z Has data issue: false hasContentIssue false
  • English
  • Français

Deriving session and union types for objects†

Published online by Cambridge University Press:  09 May 2013

LORENZO BETTINI ,
SARA CAPECCHI ,
MARIANGIOLA DEZANI-CIANCAGLINI ,
ELENA GIACHINO  and
BETTI VENNERI
LORENZO BETTINI
Affiliation:
Dipartimento di Informatica, Università di Torino, corso Svizzera 185, 10131 Torino, Italy Email: bettini@di.unito.it; capecchi@di.unito.it; dezani@di.unito.it
SARA CAPECCHI
Affiliation:
Dipartimento di Informatica, Università di Torino, corso Svizzera 185, 10131 Torino, Italy Email: bettini@di.unito.it; capecchi@di.unito.it; dezani@di.unito.it
MARIANGIOLA DEZANI-CIANCAGLINI
Affiliation:
Dipartimento di Informatica, Università di Torino, corso Svizzera 185, 10131 Torino, Italy Email: bettini@di.unito.it; capecchi@di.unito.it; dezani@di.unito.it
ELENA GIACHINO
Affiliation:
Focus Research Team, Università di Bologna/INRIA, mura Anteo Zamboni 7, 40127 Bologna, Italy Email: giachino@cs.unibo.it
BETTI VENNERI
Affiliation:
Dipartimento di Statistica, Informatica, Applicazioni, Università di Firenze, viale Morgagni 65, 50134 Firenze, Italy Email: betti.venneri@unifi.it
Get access Rights & Permissions [Opens in a new window]

Abstract

Guaranteeing that the parties of a network application respect a given protocol is a crucial issue. Session types offer a method for abstracting and validating structured communication sequences (sessions). Object-oriented programming is an established paradigm for large scale applications. Union types, which behave as the least common supertypes of a set of classes, allow the implementation of unrelated classes with similar interfaces without additional programming. We have previously developed an integration of the features above into a class-based core language for building network applications, and this successfully amalgamated sessions and methods so that data can be exchanged flexibly according to communication protocols (session types).

The first aim of the work reported in this paper is to provide a full proof of the type safety property for that core language by renewing syntax, typing and semantics. In this way, static typechecking guarantees that after a session has started, computation cannot get stuck on a communication deadlock.

The second aim is to define a constraint-based type system that reconstructs the appropriate session types of session declarations instead of assuming that session types are explicitly given by the programmer. Such an algorithm can save programming work, and automatically presents an abstract view of the communications of the sessions.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Issue 6 , December 2013 , pp. 1163 - 1219
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

This work was partially supported by MIUR Projects DISCO – Distribution, Interaction, Specification, Composition for Object Systems, and IPODS–Interacting Processes in Open-ended Distributed Systems, and by EU Collaborative project n. 257414 ASCENS – Autonomic Service-Component Ensembles.

References

Barbanera, F., Dezani-Ciancaglini, M. and de'Liguoro, U. (1995) Intersection and Union Types: Syntax and Semantics. Information and Computation 119 202–230.CrossRefGoogle Scholar
Bettini, L., Capecchi, S., Dezani-Ciancaglini, M., Giachino, E. and Venneri, B. (2008a) Session and Union Types for Object Oriented Programming. In: Concurrency, Graphs and Models. Springer-Verlag Lecture Notes in Computer Science 5065 659–680.CrossRefGoogle Scholar
Bettini, L., Coppo, M., D'Antoni, L., De Luca, M., Dezani-Ciancaglini, M. and Yoshida, N. (2008b) Global Progress in Dynamically Interleaved Multiparty Sessions. In: CONCUR'08. Springer-Verlag Lecture Notes in Computer Science 5201 418–433.CrossRefGoogle Scholar
Bettini, L., De Nicola, R. and Loreti, M. (2008c) Implementing Session Centered Calculi. In: COORDINATION'08. Springer-Verlag Lecture Notes in Computer Science 5052 17–32.CrossRefGoogle Scholar
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C. and Leifer, J. J. (2009) Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. In: Proceedings 22nd IEEE Computer Security Foundations Symposium, 2009 (CSF ‘09) 124–140.CrossRefGoogle Scholar
Bocchi, L., Honda, K., Tuosto, E. and Yoshida, N. (2010) A Theory of Design-by-Contract for Distributed Multiparty Interactions. In: CONCUR'10. Springer-Verlag Lecture Notes in Computer Science 6269 162–176.CrossRefGoogle Scholar
Bonelli, E. and Compagnoni, A. (2008) Multipoint Session Types for a Distributed Calculus. In: TGC'07. Springer-Verlag Lecture Notes in Computer Science 4912 240–256.CrossRefGoogle Scholar
Bonelli, E., Compagnoni, A. and Gunter, E. (2005) Correspondence Assertions for Process Synchronization in Concurrent Communications. Journal of Functional Programming 15 (2)219–248.CrossRefGoogle Scholar
Bono, V., Messa, C. and Padovani, L. (2011) Typing Copyless Message Passing. In: ESOP'11. Springer-Verlag Lecture Notes in Computer Science 6602 57–76.CrossRefGoogle Scholar
Capecchi, S., Castellani, I. and Dezani-Ciancaglini, M. (2011) Information Flow Safety in Multiparty Sessions. In: EXPRESS'11. Electronic Proceedings in Theoretical Computer Science 64 16–31.CrossRefGoogle Scholar
Capecchi, S., Castellani, I., Dezani-Ciancaglini, M. and Rezk, T. (2010a) Session Types for Access and Information Flow Control. In: CONCUR'10. Springer-Verlag Lecture Notes in Computer Science 6269 237–252.CrossRefGoogle Scholar
Capecchi, S., Coppo, M., Dezani-Ciancaglini, M., Drossopoulou, S. and Giachino, E. (2009) Amalgamating Sessions and Methods in Object Oriented Languages with Generics. Theoretical Computer Science 410 142–167.CrossRefGoogle Scholar
Capecchi, S., Giachino, E. and Yoshida, N. (2010b) Global Escape in Multiparty Sessions. In: FSTTCS'10. LIPIcs 8, Schloss Dagstuhl–Leibniz-Zentrum für Informatik 338–351.Google Scholar
Carbone, M., Honda, K. and Yoshida, N. (2007) Structured Communication-Centred Programming for Web Services. In: ESOP'07. Springer-Verlag Lecture Notes in Computer Science 4421 2–17.CrossRefGoogle Scholar
Carbone, M., Honda, K. and Yoshida, N. (2008a) Multiparty Asynchronous Session Types. In: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL'08) 273–284.CrossRefGoogle Scholar
Carbone, M., Honda, K. and Yoshida, N. (2008b) Structured Interactional Exceptions for Session Types. In: CONCUR'08. Springer-Verlag Lecture Notes in Computer Science 5201 402–417.CrossRefGoogle Scholar
Castagna, G., De Nicola, R. and Varacca, D. (2008) Semantic Subtyping for the π-calculus. Theoretical Computer Science 398 (1–3)217–242.CrossRefGoogle Scholar
Castagna, G., Dezani-Ciancaglini, M., Giachino, E. and Padovani, L. (2009) Foundations of Session Types. In: PPDP ‘09: Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming 219–230.CrossRefGoogle Scholar
Clarke, D., Noble, J. and Potter, J. (2001) Simple Ownership Types for Object Containment. In: ECOOP'01. Springer-Verlag Lecture Notes in Computer Science 2072 53–76.CrossRefGoogle Scholar
Coppo, M. and Dezani-Ciancaglini, M. (2009) Structured Communications with Concurrent Constraints. In: TGC'08. Springer-Verlag Lecture Notes in Computer Science 5474 104–125.CrossRefGoogle Scholar
Coppo, M., Dezani-Ciancaglini, M. and Yoshida, N. (2007) Asynchronous Session Types and Progress for Object-Oriented Languages. In: FMOODS'07. Springer-Verlag Lecture Notes in Computer Science 4468 1–31.CrossRefGoogle Scholar
Deniélou, P.-M. and Yoshida, N. (2010) Buffered Communication Analysis in Distributed Multiparty Sessions. In: CONCUR'10. Springer-Verlag Lecture Notes in Computer Science 6269 343–357.CrossRefGoogle Scholar
Dezani-Ciancaglini, M., de' Liguoro, U. and Yoshida, N. (2008) On Progress for Structured Communications. In: TGC'07. Springer-Verlag Lecture Notes in Computer Science 4912 257–275.CrossRefGoogle Scholar
Dezani-Ciancaglini, M., Drossopoulou, S., Giachino, E. and Yoshida, N. (2007) Bounded Session Types for Object-Oriented Languages. In: FMCO'06. Springer-Verlag Lecture Notes in Computer Science 4709 207–245.CrossRefGoogle Scholar
Dezani-Ciancaglini, M., Drossopoulou, S., Mostrous, D. and Yoshida, N. (2009) Session Types for Object-Oriented Languages. Information and Computation 207 (5)595–641.CrossRefGoogle Scholar
Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N. and Drossopoulou, S. (2006) Session Types for Object-Oriented Languages. In: ECOOP'06. Springer-Verlag Lecture Notes in Computer Science 4067 328–352.CrossRefGoogle Scholar
Dezani-Ciancaglini, M., Yoshida, N., Ahern, A. and Drossopoulou, S. (2005) A Distributed Object Oriented Language with Session Types. In: TGC'05. Springer-Verlag Lecture Notes in Computer Science 3705 299–318.CrossRefGoogle Scholar
Drossopoulou, S., Dezani-Ciancaglini, M. and Coppo, M. (2007) Amalgamating the Session Types and the Object Oriented Programming Paradigms. Presented at MPOOL'07.Google Scholar
Fähndrich, M., Aiken, M., Hawblitzel, C., Hodson, O., Hunt, G. C., Larus, J. R. and Levi, S. (2006) Language Support for Fast and Reliable Message-based Communication in Singularity OS. In Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006 (EuroSys2006) 177–190.CrossRefGoogle Scholar
Frisch, A., Castagna, G. and Benzaken, V. (2008) Semantic Subtyping: Dealing Set-theoretically with Function, Union, Intersection, and Negation Types. Journal of the ACM 55 (4)1–64.CrossRefGoogle Scholar
Gapeyev, V. and Pierce, B. C. (2003) Regular Object Types. In: ECOOP'03. Springer-Verlag Lecture Notes in Computer Science 2743 151–175.CrossRefGoogle Scholar
Garralda, P., Compagnoni, A. and Dezani-Ciancaglini, M. (2006) BASS: Boxed Ambients with Safe Sessions. In PPDP ‘06: Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming 61–72.CrossRefGoogle Scholar
Gay, S. (2008) Bounded Polymorphism in Session Types. Mathematical Structures in Computer Science 18 (5)895–930.CrossRefGoogle Scholar
Gay, S. and Hole, M. (2005) Subtyping for Session Types in the Pi-Calculus. Acta Informatica 42 (2/3)191–225.CrossRefGoogle Scholar
Gay, S., Vasconcelos, V. T. and Ravara, A. (2003) Session Types for Inter-Process Communication. TR 2003–133, Department of Computing, University of Glasgow.Google Scholar
Gay, S. J., Vasconcelos, V. T., Ravara, A., Gesbert, N. and Caldeira, A. Z. (2010) Modular Session Types for Distributed Object-oriented Programming. In POPL ‘10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages 299–312.CrossRefGoogle Scholar
Giachino, E. (2009) Session Types: Semantic Foundations and Object-Oriented Applications, Ph.D. thesis, Università degli Studi di Torino and Université Paris 7.Google Scholar
Honda, K. (1993) Types for Dyadic Interaction. In: CONCUR'93. Springer-Verlag Lecture Notes in Computer Science 715 509–523.CrossRefGoogle Scholar
Honda, K., Mostrous, D. and Yoshida, N. (2009) Global Principal Typing in Partially Commutative Asynchronous Sessions. In: ESOP'09. Springer-Verlag Lecture Notes in Computer Science 5502 316–332.Google Scholar
Honda, K., Vasconcelos, V. T. and Kubo, M. (1998) Language Primitives and Type Disciplines for Structured Communication-based Programming. In: ESOP'98. Springer-Verlag Lecture Notes in Computer Science 1381 22–138.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2007) Web Services, Mobile Processes and Types. EATCS Bulletin 91 160–188.Google Scholar
Hu, R., Kouzapas, D., Pernet, O., Yoshida, N. and Honda, K. (2010) Type-Safe Eventful Sessions in Java. In: ECOOP'10. Springer-Verlag Lecture Notes in Computer Science 6183 329–353.CrossRefGoogle Scholar
Hu, R., Yoshida, N. and Honda, K. (2008) Session-Based Distributed Programming in Java. In: ECOOP'08. Springer-Verlag Lecture Notes in Computer Science 5142 516–541.CrossRefGoogle Scholar
Igarashi, A. and Nagira, H. (2007) Union Types for Object Oriented Programming. Journal of Object Technology 6 (2)31–52.CrossRefGoogle Scholar
Igarashi, A., Pierce, B. C. and Wadler, P. (2001) Featherweight Java: a Minimal Core Calculus for Java and GJ. ACM TOPLAS 23 (3)396–450.CrossRefGoogle Scholar
Lieberman, H. (1986) Using Prototypical Objects to Implement Shared Behavior in Object-Oriented Systems. In: Proceedings of the 1986 conference on Object-Oriented Programming Languages, Systems and Applications: OOPLSA ‘86. SIGPLAN Notices 21 (11)214–223.CrossRefGoogle Scholar
Mostrous, D. and Yoshida, N. (2007) Two Session Typing Systems for Higher-Order Mobile Processes. In: TLCA'07. Springer-Verlag Lecture Notes in Computer Science 4583 321–335.CrossRefGoogle Scholar
Mostrous, D. and Yoshida, N. (2009) Session-Based Communication Optimisation for Higher-Order Mobile Processes. In: TLCA'09. Springer-Verlag Lecture Notes in Computer Science 5608 203–218.CrossRefGoogle Scholar
Pierce, B. C. (2002) Types and Programming Languages, MIT Press.Google Scholar
Sparkes, S. (2006) Conversation with Steve Ross-Talbot. ACM Queue 4 (2)14–23.Google Scholar
Takeuchi, K., Honda, K. and Kubo, M. (1994) An Interaction-based Language and its Typing System. In: PARLE'94. Springer-Verlag Lecture Notes in Computer Science 817 398–413.CrossRefGoogle Scholar
Vallecillo, A., Vasconcelos, V. T. and Ravara, A. (2002) Typing the Behavior of Objects and Components using Session Types. In: FOCLASA'02. Electronic Notes in Theoretical Computer Science 68 (3)439–456.CrossRefGoogle Scholar
Vasconcelos, V. T., Gay, S. and Ravara, A. (2006) Typechecking a Multithreaded Functional Language with Session Types. Theoretical Computer Science 368 (1–2)64–87.CrossRefGoogle Scholar
Web Services Choreography Working Group (2002) Web Services Choreography Description Language. (Available at http://www.w3.org/2002/ws/chor/.)Google Scholar
Yoshida, N., Deniélou, P.-M., Bejleri, A. and Hu, R. (2010) Parameterised Multiparty Session Types. In: FOSSACS'10. Springer-Verlag Lecture Notes in Computer Science 6014 128–145.CrossRefGoogle Scholar
Yoshida, N. and Vasconcelos, V. T. (2007) Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication. In: SecRet'06. Electronic Notes in Theoretical Computer Science 171 (4)73–93.CrossRefGoogle Scholar