Boxed ambients with communication interfaces
Pablo Garralda, Eduardo Bonelli, Adriana B. Compagnoni, Mariangiola Dezani-Ciancaglini · Mathematical Structures in Computer Science · 2007
We defineBACI(Boxed Ambients with Communication Interfaces), an ambient calculus with a flexible communication policy. Traditionally, typed ambient calculi have a fixed communication policy determining the kind of information that can be exchanged with a parent ambient, even though mobility changes the parent.BACIlifts that restriction, allowing different communication policies with different parents during computation. Furthermore,BACIseparates communication and mobility by making the channels of communication between ambients explicit. In contrast with other typed ambient calculi where communication policies are global, each ambient inBACIis equipped with a description of the communication policies ruling its information exchange with parent and child ambients. The communication policies of ambients increase when they move: more precisely, when an ambient enters another ambient, the entering ambient and the host ambient can exchange their communication ports and agree on the kind of information to be exchanged. This information is recorded locally in both ambients. We show the type-soundness ofBACI, proving that it satisfies the subject reduction property, and we study its behavioural semantics by means of a labelled transition system.