Computer Science Department
School of Computer Science, Carnegie Mellon University
Functional Programming with Names and Necessity
In the first part of the dissertation, I review the judgmental formulation of propositional constructive modal logic, and the definitions of necessity and possibility as universal and existential quantification over possible worlds. In the application to functional programming, possible worlds in modal logic will correspond to execution environments.
The second part investigates the notions of partial judgments; that is, judgments satisfied under some abstract condition. Partial necessity and partial possibility correspond to bounded universal and bounded existential quantification over possible worlds. While the partiality condition may be specified in several different ways, in this dissertation the focus is on the definition of partiality in terms of names. Names are labels for propositions, and a set of names represents the partiality condition obtained as a conjunction of the respective propositions.
In the third part, I discuss applications of modal logic to staged computation and metaprogramming. In these applications, it is frequently necessary to consider a primitive operation of capture-incurring substitution of program expressions into a context, which is naturally expressed in a modal type system.
The last part of the dissertation develops modal type systems for effects. The effects associated with partial possibility are those that permanently change the execution environments, and therefore must be executed in a specific linear order. Writing into a memory location is a typical example. The effects associated with partial necessity are those that may depend on the execution environment, but do not change it -- they are benign, and do not need to be specifically serialized. Examples include memory reads and control flow effects.