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.
|Advisor:||Harper, Robert, Crary, Karl|
|School:||Carnegie Mellon University|
|School Location:||United States -- Pennsylvania|
|Source:||DAI-B 69/05, Dissertation Abstracts International|
|Keywords:||Distributed computing, Mobile code, Modal logic, Modal types, Programming languages|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be