Name-Passing in an Ambient-Like Calculus and Its Proof Using Spatial Logic

We focus on the expressiveness of the restricted calculus. We show that we can still repeat Zimmer's encoding of name-passing in our calculus. Moreover, we prove a stronger operational correspon- dence result using a novel spatial logic, which specifies spatial properties of processes invariant to process reductions.