Using session types for reasoning about boundedness in the pi-calculus

The π-calculus is a well-established theoretical framework for describing mobile and parallel computation using name passing, and a central notion here is that of name binding. Unfortunately, non-trivial properties of π-calculus processes such as termination and bisimilarity are undecidable as a consequence of the fact that the calculus is Turing-powerful. The classes of depth-bounded and name-bounded processes are classes of π-calculus processes that impose constraints on how name binding is used in a process. A consequence of this is that some of the important decision problems that are undecidable for the full calculus now become decidable. However, membership of these classes of processes is undecidable, so it is difficult to make use of the positive decidability results in practice. In this paper we use binary session types to devise two type systems that give a sound and decidable characterization of each of these two properties. If a process is well-typed in our first system, it is depth-bounded. If a process is well-typed in our second, more restrictive type system, it will also be name-bounded.