Typing Linear and Non-Linear Higher-Order Mobile Embedded Resources with Local Names

We provide the first process calculus combining (affine) linear and non-linear higher-order mobile processes, nested locations, and local names. We do so by extending the type and effect system of Homer, a calculus of non-linear Higher-Order Mobile Embedded Resources, with a distinction between affine linear and non-linear locations (akin to reference types) and uses of variables (as in the linear lambda calculus). The type system guarantees that linear resources are neither copied nor embedded in non-linear resources during computation. We introduce composite reference types to guarantee that no path ever points to a linear location nested within a non-linear location. We extend the LTS semantics and adapt Howe's method to the typed setting, providing a bisimulation congruence. We apply the bisimulation to prove that scope extension across linear location boundaries is sound. Finally, we use the calculus to model an e-cash Smart Card system, the security of which depends on the interplay between (linear) mobile hardware, embedded (non-linear) mobile processes, and local names.