ABSTRACT

We present a foundational language for 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 Box and Dia to reflect mobility and locality, respectively.

We formulate a novel system of natural deduction for IS5, decomposing the introduction and elimination rules for Box and Dia, 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.