A Symmetric Modal Lambda Calculus for Distributed Computing 1 Tom Murphy VII Karl Crary Frank Pfenning March 5 2004 Robert Harper CMU CS 04 105 School of Computer Science Carnegie Mellon University Pittsburgh PA 15213 Abstract We present a foundational language for distributed programming called Lambda 5 that addresses both mobility of code and locality of resources In order to construct our system we appeal to the powerful propositions as types interpretation of logic Specifically we take the possible worlds of the intuitionistic modal logic IS5 to be nodes on a network and the connectives 2 and 3 to reflect mobility and locality respectively We formulate a novel system of natural deduction for IS5 decomposing the introduction and elimination rules for 2 and 3 thereby allowing the corresponding programs to be more direct We then give an operational semantics to our calculus that is type safe logically faithful and computationally realistic 1 The ConCert Project is supported by the National Science Foundation under grant ITR SY SI 0121633 Language Technology for Trustless Software Dissemination Keywords distributed computing lambda calculus modal logic curry howard isomorphism lambda 5 type theory programming languages 1 Introduction are provable propositions in Lambda 5 In section 4 1 we look at the actual proof terms for some of these sentences and their computational content On the other hand the following are not provable 6 A 2A Not all local values are mobile 6 3A A We cannot obtain all remote values Simpson in his Ph D thesis 15 provides an account of intuitionistic modal logic based on a generic multiple world semantics Two aspects prevent us from using his formulation directly First his system is generalized to support accessibility relations that are arbitrary geometric theories For our use of IS5 there is no useful computational content to a proof that two worlds are related We therefore dispense with judgments of the accessibility relation and simply collect a list of worlds that are mutually interaccessible The second issue requires a more significant change Simpson s rules act non locally in the sense that they often use assumptions from one world to conclude facts in another world This leads to proof terms that are inefficient at best and at worst do not even fit our computational model In section 4 5 we make this comparison concrete Our solution here is to decompose the rules for the 2 and 3 connectives into restricted rules that act locally and motion rules which extend our reasoning across world boundaries In doing so we nonetheless preserve the duality of the connectives and the desirable logical qualities as demonstrated in section 3 The remainder of the paper proceeds as follows We begin the first half by presenting our logic in judgmental style and proving standard properties about it We then present a sequent calculus based on Simpson s IS5 which admits cut and is equivalent to our system of natural deduction This yields a strong normal form theorem for our system of natural deduction validating its design In the second half of the paper we present the operational semantics of Lambda 5 based on a network abstraction For this semantics we show type safety and present several examples We conclude with a discussion of related work and plans for the future In this extended technical report we provide interesting cases of the proofs Most proofs have been mechanized in the Twelf system 12 and verified using its metatheorem checker 14 They appear in appendix B and electronically at http www cs cmu edu concert The popularity of the Internet has enabled the possibility of large scale distributed computation Distributed programming is especially popular for scientific computing tasks The goal of this paper is to present a foundational programming language for distributed computing Scientific computing tasks often require the physical distribution of computational resources and sensing instruments To be relevant our language must address both the mobility of code and the locality of fixed resources Due to aesthetic considerations we wish to take a propositions as types interpretation of an appropriate logic to form the basis of our programming language Moreover since the type systems of realistic languages such as ML and Haskell come from the same source our constructs will smoothly integrate with such languages We argue that intuitionistic modal logic forms an excellent basis for distributed computing because of its ability to represent spatial reasoning Just as propositional logic is concerned with truth modal logic is concerned with truth relative to different worlds The worlds are related by an accessibility relation whose properties distinguish different modal logics We will explain our choice of accessibility relation below Modal logic is generally concerned with two forms of propositions 2A meaning that A is true in every accessible world and 3A meaning that A is true in some accessible world Our computational interpretation realizes these worlds as the nodes in a network Because our model is a computer network where all nodes can communicate with each other equally we choose an accessibility relation that is reflexive symmetric and transitive which leads to the intuitionistic modal logic IS5 15 A value of type 2A represents mobile code of type A that can be executed at any world a value of type 3A represents the address of a remote value of type A To illustrate our interpretation we present some characteristic true propositions in IS5 and their intuitive justifications 2A A Mobile code can be executed 2A 22A Mobile code is itself mobile A 3A We can create an address for any value 33A 3A We can obtain a remote address 3A 23A Addresses are mobile values 32A 2A We can obtain a remote mobile value The last two provable propositions are especially relevant and are only true because our accessibility relation is symmetric These theorems are actually some standard axioms for a Hilbert style presentation of IS5 We opt for a judgmental presentation so all of these 2 Judgmental Lambda 5 Recall that our logic expresses truth relative to worlds Following Martin Lo f 8 we employ the notion of a hypothetical judgment which is an assertion of judgment 1 A0 A0 A A 0 A A I A A0 0 fresh 0 A 0 2A 0 fresh 3A 0 A 0 B B 3E 2I hyp A 0 A E 2A 2E A 3A 0 get 3A A 3I 3A 2A 0 fetch 2A Figure 1 Lambda 5 natural deduction nothing is known but its existence This explains the 2 introduction