Modal Types for Mobile Code (Thesis Proposal) ∗

Modal logic is a family of logics with the ability to simultaneously reason about truth from multiple perspectives. Our previous work showed how the modal logic Intuitionistic S5 could form the basis for a simple lambda calculus for spatially distributed programs. I propose here a thesis project to demonstrate the efficacy and elegance of modal type systems for controlling spatially distributed resources in a programming language. The project has strong components of both theory and practice: the design of ML5, a new programming language for distributed computing, and its implementation. I present technical details for the language and implementation where they have been completed, and a plan for the work to be done where they have not.