Logic in Computer Science (LICS 2004)

Paper: A Symmetric Modal Lambda Calculus for Distributed Computing (at LICS 2004)

Authors: Tom Murphy VII Karl Crary Robert Harper Frank Pfenning

Abstract

We present a foundational language for spatially 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 thepossible worlds of the intuitionistic modal logic IS5 to be nodes on a network, and the connectives □ and ◇ to reflect mobility and locality, respectively. We formulate a novel system of natural deduction for IS5, decomposing the introduction and elimination rules for □ and ◇, 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.

BibTeX

  @InProceedings{MurphyCraryHarperPf-ASymmetricModalLamb,
    author = 	 {Tom Murphy VII and Karl Crary and Robert Harper and Frank Pfenning},
    title = 	 {A Symmetric Modal Lambda Calculus for Distributed Computing},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {286--295},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }