Computer Science Department
School of Computer Science, Carnegie Mellon University
MOdal Typoes for Mobile Code
Tom Murphy VII
Keywords: Programming languages, thesis proposal, modal logic,
mobile code, grid computing
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.