Modal Proofs As Distributed Programs

Abstract:

We develop a new foundation for distributed programming languages by defining
an intuitionistic, modal logic and then interpreting the modal proofs as
distributed programs. More specifically, the proof terms for the various
modalities have computational interpretations as remote procedure calls, commands
to broadcast computations to all nodes in the network, commands to use portable
code, and finally, commands to invoke computational agents that can find their
own way to safe places in the network where they can execute. We prove some
simple meta-theoretic results about our logic as well as a safety theorem that
demonstrates that the deductive rules act as a sound type system for a
distributed programming language.