In this proposal, I present a calculus for distributed programming with types corresponding to necessity ([]A) and possibility (<>A) of constructive modal logic. Distributed computation has been described and studied in many ways. This work should be understood as a reconsideration of distributed programming from a new perspective --- that of modal logic and type theory.

Through a Curry-Howard interpretation of proof terms as programs and propositions as types, I show that logical necessity is connected to mobility, and possibility to (remote) locality. I give an operational interpretation based on process configurations, where each process serves as an abstract location. This semantics is type-safe, and under certain restrictions, strong normalization and confluence hold.

The notions of mobility and locality derived from modal logic are general and open-ended. I present some extensions and examples, including examples of mobile and localized values. Finally, I discuss plans to implement the calculus for execution in the the ConCert grid computing framework and characteristics of S4 modal logic (among other logics) which involve trade-offs between expressive power and feasibility of implementation.