Typing Services

The notion of a session is fundamental in service-oriented applications, as it serves to separate interactions between clients and different instances of the same service, and to group together logical units of work. In the area of process calculi Honda, Kubo and Vasconcelos proposed their perspective of what a session should be from the perspective of theorical foundations. They presented a calculus equipped with a notion of session types that govern the interactions between peers. This first proposal gave rise to a new research direction and to a community of researchers interested in session types and their extensions and applications. The great merit of session types is in fact to be like a classical type system, intended to describe structural properties of the data manipulated by programs. One can think of a session type as the equivalent notion of channel sorting for the π-calculus. The novelty is that well-typedness of a process implies a stronger property than any other classical type systems, namely the session safety. Session safety guarantees that at runtime any interaction inside a session will proceed without errors due to mismatching communications. Moreover, with a little additional effort, session safety implies the progress property, which in some manner prevents deadlock. Well typing of a process written in a session calculus can be easily verified at the cost to annotate certain names of the processes with session types. Here we address the problem of finding efficient procedure for checking well-typedness in absence of any type annotation or said in other words the type inference of session types. It is interesting how different notions proposed in different works on session types are used together as tools to achieve the result. At the end our study leads to establish a formal theory of session types that can be applied and transferred to various settings and formalisms. Since type inference strictly depends on a specific calculus we show the wide applicability of our result studying the problem for two particular calculi with very different mechanisms of session instantiation. Prototype implementation of the type algorithms are written in Ocaml and available at http://www.di.unipi.it/-mezzina.