How to infer finite session types in a calculus of services and sessions

Abstract

The notion of session is fundamental in service oriented applications, as it separates interactions between different instances of the same service, and it groups together basic units of work. Together with sessions, session types were introduced to track the type of the values exchanged in each session. In this paper we propose an algorithm to infer a restricted form of session types and we show that the problem is not directly related to the unification since we are in a context with duality in interactions. The discussion is based on a SCC-like [3] calculus adapted to fit session types. The calculus simplifies the discussion imposing strong syntactic constraints, but the ideas and the proposed algorithm can be adopted to study the type inference for other session oriented calculi. Also an OCaml prototype of the algorithm has been developed to show its feasibility. © 2008 Springer-Verlag Berlin Heidelberg.