A modal language for the safety of mobile values

Abstract

In the context of distributed computations, local resources give rise to an issue not found in stand-alone computations: the safety of mobile code. One approach to the safety of mobile code is to build a modal type system with the modality □ that corresponds to necessity of modal logic. We argue that the modality □ is not expressive enough for safe communications in distributed computations, in particular for the safety of mobile values. We present a modal language which focuses on the safety of mobile values rather than the safety of mobile code. The safety of mobile values is achieved with a new modality □ which expresses that given code evaluates to a mobile value. We demonstrate the use of the modality □ with a communication construct for remote procedure calls. © Springer-Verlag Berlin Heidelberg 2006.