Types, Dependency and Safety of Concurrent Languages with Communications 

Nobuko Yoshida



Abstract

In this talk, we shall focus on static checking of interference and
dependency analysis of communication protocols which are described by
some popular languages, such as Java and Web Description Languages. It
is also related to security --- liveness, deadlock freedom and
noninterference when the value or channels are passed around among
different participants (roles).

This talk first gives an overview of the past and current studies of
types of mobile processes connecting with dependency and interference.
Then we shall talk about session types which are now widely developed
for the pi-calculus, Ambient, CORBA interfaces, multi-threaded
functional languages, Web Description languages, and concurrent and
distributed Java.  In particular, the second part of the talk shall
focus on the incorporation of session types into a multi-threaded
object-oriented language, which has thread spawning, iterative and
higher-order sessions.  We show by static checking using session
types, our language can guarantee communication error freedom and
deadlock-freedom on communication channels: once a communication has
been established, well-typed programs will never starve at
communication points.