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

AbstractThis paper studies a restricted version of the ambient calculus. We only allow single-threaded ambients migrating in a network of immobile ambients, exchanging payloads, and delivering them. With this restriction, we arrive at a calculus free from grave interferences. In previous works, this is only possible by sophisticated type systems.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