Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Typing Services
Leonardo Gaetano Mezzina
abstract:
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.
