Abstract

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.