Computer Science Department
School of Computer Science, Carnegie Mellon University


A Symmetric Modal Lambda Calculus for Distributed Computing

Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning

March 2004

Keywords: Distributed computing, lambda calculus, modal logic, curry-howard isomorphism, Lambda 5, type theory, programming languages

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 [] 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.

31 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by