A distributed object-oriented language with session types

In the age of the world-wide web and mobile computing, programming communication-centric software is essential. Thus, programmers and program designers are exposed to new levels of complexity, such as ensuring the correct composition of communication behaviours and guaranteeing deadlock-freedom of their protocols. This paper proposes the language L-doos, a simple distributed object-oriented language augmented with session communication primitives and types. L-doos provides a flexible object-oriented programming style for structural interaction protocols by prescribing channel usages within signatures of distributed classes. We develop a typing system for L-doos and prove its soundness with respect to the operational semantics. We also show that in a well-typed Ldoos program, there will never be a connection error, a communication error, nor an incorrect completion between server-client interactions. These results demonstrate that a consistent integration of object-oriented language features and session types can statically check the consistent composition of communication protocols.