We present a foundational language for distributed programming, called
\lfive, that addresses both mobility of code and locality of resources.

In order to construct our system, we appeal to the powerful
\emph{propositions-as-types} interpretation of logic. Specifically, we
take the \emph{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.