Sciweavers

CSL
2005
Springer

Distributed Control Flow with Classical Modal Logic

13 years 11 months ago
Distributed Control Flow with Classical Modal Logic
In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. With the modalities P and Q we were able to capture two key invariants: the mobility of portable code and the locality of fixed resources. 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 PA ≡ ¬Q¬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.
Tom Murphy VII, Karl Crary, Robert Harper
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CSL
Authors Tom Murphy VII, Karl Crary, Robert Harper
Comments (0)