Deriving Session and Union Types for Objects

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 implementing 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, which successfully amalgamates sessions and methods in order to flexibly exchange data according to communication protocols (session types). The first aim of this work is to provide a full proof of the type safety property for that core language, by renewing syntax, typing and semantics. Hence 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 which reconstructs the appropriate session types of session declarations, instead of assuming that session types are explicitly given by the programmer; such algorithm can save programming work, and automatically presents an abstract view of the communications of the sessions.