A Distributed Object-Oriented Language with Session Types

Abstract:

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 L_doos 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 offers a compositional method to statically check safety of communication protocols.