Computer Science Department
School of Computer Science, Carnegie Mellon University
A Modal Language for the Safety of Mobile Values
Keywords: Modal language, distributed computation, type system
We present a modal language for distributed computation which
addresses the safety of mobile values as well as mobile code.
The safety of mobile code is achieved with the modality 
which corresponds to necessity of modal logic. For the safety
of mobile values, we introduce a new modality Ο which expresses
that given code evaluates to a mobile value. We demonstrate
the use of modal types with three communication constructs:
remote evaluation, futures, and asynchronous channels.