Typing and Subtyping Mobility in Boxed Ambients
Massimo Merro and Vladimiro Sassone
We provide a novel type system for ambients that combines value subtyping with mobility types. The former is based on input/output channel types, while the latter builds on the notion of ambient group. Ambient types specify new group-based mobility constraints - such as where the ambient is allowed to stay and who can exit its boundaries - and close existing expressiveness gaps in the literature at no additional costs in terms of complexity. Subtyping is aimed at achieving maximal generality both on mobility and communication types.