Modular session types for distributed objectoriented programming

Abstract. 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 dis-tributed object-oriented languages by allowing a session (protocol) imple-mentation to be modularized: it can be separated into separately-callable methods. We achieve this by integrating session-typed communication channels into a type system for non-uniform objects, based on a form of typestates. We formalize a small distributed class-based object-oriented language in which static typing guarantees that both sequences of mes-sages on channels, and sequences of method calls on objects, conform to type-theoretic specifications. The formalization includes both a type system and a typechecking algorithm. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as inheritance. We also describe a prototype implementation as an extension of Java.