Distributed Control Flow with Classical Modal Logic
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.
KeywordsModal Logic Classical Logic Operational Semantic Natural Deduction Proof Theory
Unable to display preview. Download preview PDF.
- 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.Girard, J.-Y.: Towards a geometry of interaction. Contemporary Mathematics 92, 69–108Google Scholar
- 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.Jia, L., Walker, D.: Modal proofs as distributed programs. In: 13th European Symposium on Programming, March 2004, pp. 219–223 (2004)Google Scholar
- 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.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.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.Murthy, C.: Classical proofs as programs: How, what and why. Technical Report TR91-1215, Cornell University (1991)Google Scholar
- 14.Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)Google Scholar
- 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