We define a language with a functional core and constructs for transmitting and receiving values across remote sites in which mobile agents have a natural representation as function closures. We present the dynamic semantics of this language in relational style. We develop a static type and effect system where the types are annotated so that the effects expose potentially mobile functions and channels. Finally, we prove the consistency of this system with respect to the dynamic semantics.
This report is available in the following formats: