A Calculus of Higher Order Safe Ambients and Its Bisimulations

In this paper, we present a higher order ambient calculus HSAP, which is a higher order extension of SAP calculus. In HSAP, we extend higher order communication capability and administrator interaction capability. Higher order communication capability means that an ambients can be send to another ambients. Administrator interaction capability means that an ambients can interact with any ambients if the password is matched. Then, we give a LTS based operational semantics for HSAP and two labelled bisimulations, called early bisimulation and late bisimulation. Early bisimulation is proved to coincide with reduction barbed congruence. Furthermore, we present late bisimulation, quasi late bisimulation, concise quasi late bisimulation and quasi normal bisimulation for HSAP and study the relation between these bisimulations. Finally, we study the expressiveness of HSAP.