The m-calculus: a higher-order distributed process calculus

ABSTRACT

This paper presents a new distributed process calculus, called the M-calculus, that can be understood as a higher-order version of the Distributed Join calculus with programmable localities. The calculus retains the implementable character of the Distributed Join calculus while overcoming several important limitations: insufficient control over communication and mobility, absence of dynamic binding, and limited locality semantics. The calculus is equipped with a polymorphic type system that guarantees the unicity of locality names, even in presence of higher-order communications -- a crucial property for the determinacy of message routing in the calculus.

REFERENCES

• 1: R. Amadio. An asynchronous model of locality, failure, and process mobility. Technical report, INRIA Research Report RR-3109, INRIA Sophia-Antipolis, France, 1997.
• 2: Michele Bugliesi , Giuseppe Castagna , Silvia Crafa, Boxed Ambients, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.38-63, October 29-31, 2001
• 3: Luca Cardelli , Andrew D. Gordon, Types for mobile ambients, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.79-92, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292550]
• 4: Luca Cardelli , Andrew D. Gordon, Mobile Ambients, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure, p.140-155, March 28-April 04, 1998
• 5: Dominic Duggan, Atomic failure in wide-area computation, Fourth International Conference on Formal methods for open object-based distributed systems IV, p.65-86, September 2000, Stanford, California, United States
• 6: C. Fournet. The Join-Calculus. PhD thesis, Ecole Polytechnique, 1998.
• 7: Cédric Fournet , Georges Gonthier , Jean-Jacques Lévy , Luc Maranget , Didier Rémy, A Calculus of Mobile Agents, Proceedings of the 7th International Conference on Concurrency Theory, p.406-421, August 26-29, 1996
• 8: Cédric Fournet , Jean-Jacques Lévy , Alan Schmitt, An Asynchronous, Distributed Implementation of Mobile Ambients, Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, p.348-364, August 17-19, 2000
• 9: F. Germain, M. Lacoste, and J.B. Stefani. An abstract machine for a higher-order distributed process calculus. In Proceedings of the EACTS Workshop on Foundations of Wide Area Network Computing (F-WAN), July 2002.
• 10: Francesca Levi , Davide Sangiorgi, Controlling interference in ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.352-364, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325741]
• 11: Jean-Jacques Lévy, Some Results in the Joint-Calculus, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.233-249, September 23-26, 1997
• 12: L. Lopes, F. Silva, A. Figueira, and V. Vasconcelos. DiTyCO: An Experiment in Code Mobility from the Realm of Process Calculi. In Proceedings 5th Mobile Object Systems Workshop (MOS'99), 1999.
• 13: Massimo Merro , Matthew Hennessy, Bisimulation congruences in safe ambients, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-80, January 16-18, 2002, Portland, Oregon
• 14: Rocco de Nicola , Gian Luigi Ferrari , Rosario Pugliese, KLAIM: A Kernel Language for Agents Interaction and Mobility, IEEE Transactions on Software Engineering, v.24 n.5, p.315-330, May 1998 [doi>10.1109/32.685256]
• 15: Rocco De Nicola , GianLuigi Ferrari , Rosario Pugliese , Betti Venneri, Types for access control, Theoretical Computer Science, v.240 n.1, p.215-254, June 6 2000 [doi>10.1016/S0304-3975(99)00232-7]
• 16: Didier Rémy, Type inference for records in natural extension of ML, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994
• 17: Davide Sangiorgi , Andrea Valente, A Distributed Abstract Machine for Safe Ambients, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.408-420, July 08-12, 2001
• 18: A. Schmitt and J.B. Stefani. The M-calculus: A Higher Order Distributed Process Calculus. Draft of the long version, available at http://pauillac.inria.fr/~aschmitt/publications.html, 2002.
• 19: Alan Schmitt. Conception et Implmentation de Calculs d'Agents Mobiles. PhD thesis, Ecole Polytechnique, 2002.
• 20: Alan Schmitt, Safe Dynamic Binding in the Join Calculus, Proceedings of the IFIP 17th World Computer Congress - TC1 Stream / 2nd IFIP International Conference on Theoretical Computer Science: Foundations of Information Technology in the Era of Networking and Mobile Computing, p.563-575, August 25-30, 2002
• 21: Peter Sewell , Jan Vitek, Secure composition of untrusted code: box π, wrappers, and causality types, Journal of Computer Security, v.11 n.2, p.135-187, May 2003
• 22: David Teller , Pascal Zimmer , Daniel Hirschkoff, Using Ambients to Control Resources, Proceedings of the 13th International Conference on Concurrency Theory, p.288-303, August 20-23, 2002
• 23: Jan Vitek , Giuseppe Castagna, Seal: A Framework for Secure Mobile Computations, Workshop on Internet Programming Languages, p.47-77, May 13, 1998
• 24: Pawel T. Wojciechowski , Peter Sewell, Nomadic Pict: Language and Infrastructure Design for Mobile Agents, IEEE Concurrency, v.8 n.2, p.42-52, April 2000 [doi>10.1109/4434.846193]
• 25: Nobuko Yoshida , Matthew Hennessy, Suptyping and Locality in Distributed Higher Order Processes (extended abstract), Proceedings of the 10th International Conference on Concurrency Theory, p.557-572, August 24-27, 1999
• 26: Nobuko Yoshida , Matthew Hennessy, Assigning Types to Processes, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.334, June 26-29, 2000

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.m MISCELLANEOUS

General Terms:
Design, Languages, Theory

Keywords:
distribution, higher order, mobility, process calculi, type systems