Abstract:

We provide a novel type system for ambients that combines value
subtyping with mobility types.
The former is based on read/write exchange 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. We then introduce
co-capabilities to express explicit permissions to access an
ambient. In this setting, we can specify who is allowed to enter an
ambient.