A symmetric modal lambda calculus for distributed computing

We present a foundational language for spatially distributed programming, called Lambda 5, that addresses both mobility of code and locality of resources. In order to construct our system, we appeal to the powerful propositions-as-types interpretation of logic. Specifically, we take the possible worlds of the intuitionistic modal logic IS5 to be nodes on a network, and the connectives □ and ◊ to reflect mobility and locality, respectively. We formulate a novel system of natural deduction for IS5, decomposing the introduction and elimination rules for □ and ◊, thereby allowing the corresponding programs to be more direct. We then give an operational semantics to our calculus that is type-safe, logically faithful, and computationally realistic.