Tom Murphy VII

Modal Types for Mobile Code Degree Type: Ph.D. in Computer Science
Advisor(s): Robert W. Harper, Karl Crary
Graduated: May 2008

Abstract:

In this dissertation I argue that modal type systems provide an elegant and practical means for controlling local resources in spatially distributed computer programs. A distributed program is one that executes in multiple physical or logical places. It usually does so because those places have local resources that can only be used in those locations. Such resources can include processing power, proximity to data, hardware, or the physical presence of a user. Programmers that write distributed applications therefore need to be able to reason about the places in which their programs will execute. This work provides an elegant and practical way to think about such programs in the form of a type system derived from modal logic.

Modal logic allows for reasoning about truth from multiple simultaneous perspectives. These perspectives, called "worlds," are identified with the locations in the distributed program. This enables the programming language to be simultaneously aware of the various hosts involved in a program, their local resources, and their differing perspectives on each other's code and data. This leads to a clean and general type structure for programs that respects locality while permitting high-level language features. To argue that this system is elegant, I present a modal logic formulated for this purpose and then prove its global soundness and completeness and its equivalence to known logics. I then show how a small programming language can be derived from the logic, and how it can be implemented, proving properties of this abstract compilation procedure. All of these theorems are formalized in Twelf and can be checked by computer. To demonstrate that it is practical, I then extend the modal calculus to a full-fledged programming language based on ML. I implemented a compiler for this language for the specific case of web applications, a distributed computation involving two hosts with widely different capabilities: the web server and the web browser. I then use the completed implementation to build realistic web applications.

Thesis Committee:
Robert Harper (Co-Chair)
Karl Crary (Co-Chair)
Frank Pfenning
Peter Sewell

Peter Lee, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
modal logic, distributed computing, programming languages, web programming, compilers, types