Computer Science Department
School of Computer Science, Carnegie Mellon University
Distributed Control Flow with Classical Modal Logic
Tom Murphy VII, Karl Crary, Robert Harper
This work investigates issues in distributed control flow through a similar propositions-as-types interpretation of classical modal logic. The resulting programming language is enhanced with the notion of a network-wide continuation, through which we can give computational interpretation of classical theorems (such as box A being equivalent to not diamond not A). Such continuations are also useful primitives for building higher-level constructs of distributed computing. The resulting system is elegant, logically faithful, and computationally reasonable.