We extend Kobayashi and Sumii's type system for the deadlock-free
Pi-calculus and develop a type reconstruction algorithm. Kobayashi
and Sumii's type system is a generalization of Kobayashi, Pierce, and
Turner's linear pi-calculus, and it helps high-level reasoning about
concurrent programs by guaranteeing that communication on certain
channels will eventually succeed. It can ensure, for example, that a
process implementing a function really behaves like a function.
However, because it lacked a type reconstruction algorithm and
required rather complicated type annotations, it was impractical to
apply it to real concurrent languages. We have therefore developed a
type reconstruction algorithm for an extension of the type system. The
key novelties that made it possible are generalization of the channel
usage calculus (which was first introduced in Sumii and Kobayashi's
previous type system) and a subusage relation.