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. © Springer-Verlag 2004.