There is a gap between theory and implementation of the pi calculus. It relates to the nu command, also called restriction. In typical implementations of process calculi (Pict, chemical abstract machine) the command allocates a new communication channel. This amounts to discarding top-level restrictions and dispensing with scope extrusion; it yields a very simple multiset or chemical solution semantics. In contrast, the pi calculus and the join calculus retain restriction and scope extrusion. The gap has previously been finessed or glossed over. We state the gap formally and prove that, for pi, scopes and fresh name generation are equally expressive up to full abstraction.
@Misc{wis04_oldnames,
author = "Lucian Wischik",
title = "Old Names for Nu",
year = 2004,
note = "Presented at Dagstuhl Seminar 04241",
url = "http:// www.wischik.com/ lu/ research/ oldnames.html",
}
Note: apparently some similar work also appeared in a Japanese paper. I don't have details.