A Modal Language for the Safety of Mobile Values Seminars/Workshops

Abstract

I will present a modal language for distributed computation which addresses the safety of mobile values as well as mobile code. Unlike traditional approaches, my work focuses on the safety of mobile values rather than mobile code, since the safety of mobile code M is easy to verify by checking the safety of a mobile value Lam _. M. For the safety of mobile values, we introduce two new modalities which express that given code evaluates to a mobile value. The first modality is used to ensure that given code evaluates to a mobile value that is valid at any node in the network; it is similar in nature to the necessity modality of modal logic. The second is used to ensure that given code evaluates to a mobile value that is valid at a certain node in the network; it is similar in nature to the possibility modality of modal logic.

If time permits, I will describe a logic of direct evidence, a new form of modal logic inspired by this work.