Types for Mobile Ambients

Java has demonstrated the utility of type systems for mobile code, and in particular their use and implications for security.  Security properties rest on the fact that a well-typed Java program (or the corresponding verified bytecode) cannot cause certain kinds of damage.  In this paper we provide a type system for mobile computation, that is, for computation that is continuously active before and after movement.  We show that a well-typed mobile computation cannot cause certain kinds of run-time fault: it cannot cause the exchange of values of the wrong kind, anywhere in a mobile system.