Distributed Control Flow with Classical Modal Logic

  • Tom Murphy VII
  • Karl Crary
  • Robert Harper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. With the modalities □ and \(\Diamond\) we were able to capture two key invariants: the mobility of portable code and the locality of fixed resources. This work investigates issues in distributed control flow through a similar propositions-as-types interpretation of classical modal logic. The resulting programming language is enhanced with the notion of a network-wide continuation, through which we can give computational interpretation of classical theorems (such as \(\Box A \equiv \lnot \Diamond \lnot A\)). Such continuations are also useful primitives for building higher-level constructs of distributed computing. The resulting system is elegant, logically faithful, and computationally reasonable.


Modal Logic Classical Logic Operational Semantic Natural Deduction Proof Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abel, A.: A third-order representation of the λμ-Calculus. In: Ambler, S.J., Crole, R.L., Momigliano, A. (eds.) Electronic Notes in Theoretical Computer Science, vol. 58, Elsevier, Amsterdam (2001)Google Scholar
  2. 2.
    Girard, J.-Y.: Towards a geometry of interaction. Contemporary Mathematics 92, 69–108Google Scholar
  3. 3.
    Girard, J.-Y.: Linear logic. Theoretical Computer Science 50(1), 1–102 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Griffin, T.G.: The formulae-as-types notion of control. In: Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL 1990, San Francisco, CA, USA, January 17-19, pp. 47–57. ACM Press, New York (1990)Google Scholar
  5. 5.
    Jia, L., Walker, D.: Modal proofs as distributed programs. In: 13th European Symposium on Programming, March 2004, pp. 219–223 (2004)Google Scholar
  6. 6.
    Moody, J.: Modal logic as a basis for distributed computation. Technical Report CMU-CS-03-194, Carnegie Mellon University (October 2003)Google Scholar
  7. 7.
    Murphy VII, T., Crary, K., Harper, R.: Distribed control flow with classical modal logic (technical report). Technical Report CMU-CS-04-177, Carnegie Mellon University (December 2004) Google Scholar
  8. 8.
    Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), July 2004, IEEE Press, Los Alamitos (2004)Google Scholar
  9. 9.
    Murthy, C.: Classical proofs as programs: How, what and why. Technical Report TR91-1215, Cornell University (1991)Google Scholar
  10. 10.
    Parigot, M.: λμ-Calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, Springer, Heidelberg (1992)CrossRefGoogle Scholar
  11. 11.
    Pfenning, F., Schürmann, C.: System description: Twelf – a metalogical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  12. 12.
    Reppy, J.H.: Concurrent Programming in ML. Cambridge University Press, Cambridge (1999)CrossRefGoogle Scholar
  13. 13.
    Schürmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 120–135. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)Google Scholar
  15. 15.
    Wadler, P.: Call-by-value is dual to call-by-name. In: Proceedings of the 8th International Conference on Functional Programming (ICFP), August 2003, ACM Press, New York (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Tom Murphy VII
    • 1
  • Karl Crary
    • 1
  • Robert Harper
    • 1
  1. 1.Carnegie Mellon University 

Personalised recommendations