Abstract
Deadlock is one of the most serious problems in concurrent
programming. Recently, Kobayashi proposed a static type system for a
process calculus which ensures that communication over some special
channels never causes deadlock. However, since the class of such
channels was fixed ad hoc by the type system, the deadlock-free
fragment of the calculus was limited and the essence of the type
system was not so clear.
In this paper, we generalize his type system in order to extend the
deadlock-free part of his calculus. For that purpose, we annotate
each channel type with an expression called a \emph{usage}, which
specifies how the channel \emph{may} and \emph{must} be used. It is
automatically checked by the type system that the usage does not cause
deadlock and that the channel is actually used along the
specification. As a result, the deadlock-freedom property is treated
more uniformly and guaranteed more extensively.