View article

We consider πI, a fragment of the π-calculus where only exchange of private names among processes is permitted (internal mobility). The calculus πI enjoys a simpler mathematical treatment, very close to that of CCS. In particular, πI avoids the concept of substitution. We provide an encoding from the asynchronous π-calculus to πI and then prove that two processes are barbed-equivalent in π-calculus if and only if their translations in πI cannot be distinguished, under barbed bisimilarity, by any translated static context. The result shows that, in namepassing calculi, internal mobility is the essential ingredient as far as expressiveness is concerned.