Abstract
We extend a previous type system for the pi-calculus that
guarantees deadlock-freedom. The previous type systems for
deadlock-freedom either lacked a reasonable type inference algorithm or
were not strong enough to ensure deadlock-freedom of processes using
recursion. Although the extension is fairly simple, the new type
system admits type inference and is much more expressive than the
previous type systems that admit type inference. In fact, we show that
the simply-typed lambda-calculus with recursion can be encoded into
the deadlock-free fragment of our typed pi-calculus. To enable analysis
of realistic programs, we also present an extension of the type system to
handle recursive data structures like lists.
Both extensions have already been incorporated into the recent release
of TyPiCal, a type-based analyzer for the pi-calculus.