Type inference for a distributed π-calculus

We study the type inference problem for a distributed π-calculus with explicit notions of locality and migration. Location types involve names that may be bound in terms. This requires an accurate new approach. We define a notion of principal typing. We provide a formal description of a sound and complete type inference algorithm.