
CMUCS04105
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS04105
A Symmetric Modal Lambda Calculus for Distributed Computing
Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
March 2004
CMUCS04105.ps
CMUCS04105.pdf
Keywords: Distributed computing, lambda calculus, modal logic,
curryhoward 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
propositionsastypes 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 typesafe, logically
faithful, and computationally realistic.
31 pages
