zbMATH — the first resource for mathematics

A modal language for the safety of mobile values. (English) Zbl 1168.03327
Kobayashi, Naoki (ed.), Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8–10, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48937-5/pbk). Lecture Notes in Computer Science 4279, 217-233 (2006).
Summary: 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 \(\square\) that corresponds to necessity of modal logic. We argue that the modality \(\square\) 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 \(\boxdot\) which expresses that given code evaluates to a mobile value. We demonstrate the use of the modality \(\boxdot\) with a communication construct for remote procedure calls.
For the entire collection see [Zbl 1133.68007].
03B70 Logic in computer science
03B45 Modal logic (including the logic of norms)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Full Text: DOI