Modal proofs as distributed programs

Imin Jia, David Walker

Research output: Chapter in Book/Report/Conference proceedingChapter

29 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsDavid Schmidt
PublisherSpringer Verlag
Pages219-233
Number of pages15
ISBN (Print)3540213139, 9783540213130
DOIs
StatePublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2986
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Modal proofs as distributed programs'. Together they form a unique fingerprint.

Cite this