Abstract
We propose a general, powerful framework of type systems for the
pi-calculus, and show that we can obtain as its instances a variety of
type systems guaranteeing non-trivial properties like deadlock-freedom
and race-freedom. A key idea is to express types and type environments
as abstract processes: We can check various properties of a process by
checking the corresponding properties of its type environment. The
framework clarifies the essence of recent complex type systems, and it
also enables sharing of a large amount of work such as a proof of type
preservation, making it easy to develop new type systems.