Types and deadlock free sessions for SCC

The notion of a session is fundamental in service oriented
applications, as it serves to separate
interactions between different instances of the same services, and
to group together logical units of work. Recently, SCC has been
proposed as a calculus centered around the concept of a dyadic
session, where service interaction protocols and service
orchestration can be conveniently expressed. In this paper we
propose a generic type system to collect services' behaviors and then we fix a class of well typed processes that are guaranteed to be deadlock free. The type system is based on
previous research on traditional mobile calculi,
here conveniently extended and simplified thanks to the neat
discipline imposed by the linguistic primitives of SCC.