Computing Publications

Publications Home » Session Types for Object-Oriented...

Session Types for Object-Oriented Languages

Dezani Dezani-Ciancaglini, Dimitrios Mostrous, Nobuko Yoshida, Sophia Drossopoulou

Conference or Workshop Paper
20th European Conference for Object-Oriented Languages
July, 2006
Springer Verlag

A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other party. Session types characterise such sessions in terms of the types of values communicated and the shape of protocols, and have been developed for the pi-calculus, CORBA interfaces, and functional languages. We study the incorporation of session types into object-oriented languages through the language 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 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.

PDF of full publication (289 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.