Names of the Pi-Calculus Agents Handled Locally

We address the problem of handling names in concurrent and distributed systems made up of mobile processes. We equip processes with local environments. Our structural operational semantics handles these environments so that captures of names are never possible. Our semantics includes the specification of a distributed name manager that conservatively extends standard operational semantics. Bisimulation-based equivalences can be checked on our transition systems. They yield the same equivalence relations as those based on standard interleaving semantics. Finally, we show that our development scales up smoothly to higher-order calculi.