Abstract
We present a type theory characterizing the mobility and locality of program terms in a distributed computation. The type theory of our calculus is derived from logical notions of necessity (□A) and possibility (\(\lozenge A\)) of the modal logic S4 via a Curry-Howard style isomorphism. Logical worlds are interpreted as sites for computation, accessibility corresponds to dependency between processes at those sites. Necessity (□A) describes terms of type A which have a structural kind of mobility or clocation-independence. Possibility (\(\lozenge A\)) describes terms of type A located somewhere, perhaps at a remote site. The modalities □ and \(\lozenge\) are defined in a clean, orthogonal manner, leading to a simple account of mobility and higher-order functions. For illustration, we assume an execution environment with each location distinguished by a mutable store. Here modal types ensure that store addresses never escape from the location where they are defined, eliminating a source of runtime errors. We speculate as to other advantages or trade-offs of this disciplined style of distributed programming.
Keywords
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Borghuis, T., Feijs, L.: A constructive logic for services and information flow in computer networks. The Computer Journal 43(4) (2000)
Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 1–37. Springer, Heidelberg (2001)
Caires, L., Cardelli, L.: A spatial logic for concurrency (part II). In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 209–225. Springer, Heidelberg (2002)
Cardelli, L., Ghelli, G., Gordon, A.D.: Mobility types for mobile ambients. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 230–239. Springer, Heidelberg (1999)
Cardelli, L., Ghelli, G., Gordon, A.D.: Mobility types for mobile ambients. Technical Report MSR-TR-99-32, Microsoft (June 1999)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Cardelli, L., Gordon, A.D.: Logical properties of name restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 46–60. Springer, Heidelberg (2001)
Cardelli, L., Gordon, A.D.: Ambient logic. Technical report, Microsoft (2002)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173, 82–120 (2002)
Jagannathan, S.: Continuation-based transformations for coordination languages. Theoretical Computer Science 240(1), 117–146 (2000)
Jia, L., Walker, D.: Modal proofs as distributed programs. Technical Report TR-671-03, Princeton University (August 2003)
Jia, L., Walker, D.: Modal proofs as distributed programs. In: European Symposium on Programming Languages (April 2004)
Kranz, D.A., Halstead Jr., R.H., Mohr, E.: Mul-T: a high-performance parallel lisp. In: Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, pp. 81–90. ACM Press, New York (1989)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (I & II). Information and Computation 100(1), 1–77 (1992)
Moody, J.: Modal logic as a basis for distributed computation. Technical Report CMU-CS-03-194, Carnegie Mellon University (October 2003)
Moody, J.: Logical mobility and locality types (extended report). Technical Report CMU-CS-05-128, CMU (2005)
De Nicola, R., Ferrari, G., Pugliese, R., Venneri, B.: Types for access control. Theoretical Computer Science 240(1), 215–254 (2000); Klaim and tuple-spaces
Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11(4), 511–540 (2001)
Ravara, A., Matos, A.G., Vasconcelos, V.T., Lopes, L.: Lexically scoped distribution: what you see is what you get. In: Foundations of Global Computing. Elsevier, Amsterdam (2003)
Simpson, A.K.: Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)
Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. In: LICS (2004) (to appear)
Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. Technical Report CMU-CS-04-105, Carnegie Mellon University (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moody, J. (2005). Logical Mobility and Locality Types. In: Etalle, S. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2004. Lecture Notes in Computer Science, vol 3573. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11506676_5
Download citation
DOI: https://doi.org/10.1007/11506676_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26655-6
Online ISBN: 978-3-540-31683-1
eBook Packages: Computer ScienceComputer Science (R0)