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 thepossible 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.