Towards a primitive higher order calculus of broadcasting systems

ABSTRACT

Ethernet-style broadcast is pervasive style of computer communication.In this style,the medium is single nameless channel.Previous work on modelling such systems proposed .rst order process calculus called CBS.In this paper, we propose fundamentally different calculus called HOBS.Compared to CBS, HOBS 1) is higher order rather than first order, 2) supports dynamic subsystem encapsulation rather than static,and 3) does not require an "underlying language" to be Turing-complete. Moving to higher order calculus is key to increasing the expressivity of the primitive calculus and alleviating the need for an underlying language. The move, however, raises the need for significantly more machinery to establish the basic properties of the new calculus.This paper develops the basic theory for HOBS and presents two example programs that illustrate programming in this language. The key technical underpinning is an adaptation of Howe's method to HOBS to prove that bisimulation is congruence. From this result, HOBS is shown to embed the lazy λ-calculus.

REFERENCES

• 1: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 2: Bryan Bayerdorffer. Distributed programming with associative broadcast.In Proceedings of the 27th Annual Hawaii International Conference on Systems Sciences volume 2:Software Technology (HICSS92-2), pages 353--362, Wailea, HW, USA, 1994.
• 3: Luca Cardelli , Giorgio Ghelli , Andrew D. Gordon, Secrecy and Group Creation, Proceedings of the 11th International Conference on Concurrency Theory, p.365-379, August 22-25, 2000
• 4: Luca Cardelli , Andrew D. Gordon, Mobile ambients, Theoretical Computer Science, v.240 n.1, p.177-213, June 6 2000 [doi>10.1016/S0304-3975(99)00231-5]
• 5: Cristian Ene , Traian Muntean, Expressiveness of Point-to-Point versus Broadcast Communications, Proceedings of the 12th International Symposium on Fundamentals of Computation Theory, p.258-268, August 30-September 03, 1999
• 6: Cristian Ene and Traian Muntean. A broadcast-based calculus for communicating systems. In 6th International Workshop on Formal Methods for Parallel Programming:Theory and Applications, San Francisco, 2001.
• 7: William Ferreira , Matthew Hennessy , Alan Jeffrey, A theory of weak bisimulation for Core CML, Journal of Functional Programming, v.8 n.5, p.447-491, September 1998 [doi>10.1017/S0956796898003165]
• 8: Cédric Fournet , Georges Gonthier, The reflexive CHAM and the join-calculus, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.372-385, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237805]
• 9: Andrew D. Gordon. Bisimilarity as a theory of functional programming: mini-course. Notes Series BRICS-NS-95-3, BRICS, Department of Computer Science,University of Aarhus,July 1995.
• 10: Douglas J. Howe, Proving congruence of bisimulation in functional programming languages, Information and Computation, v.124 n.2, p.103-112, Feb. 1, 1996 [doi>10.1006/inco.1996.0008]
• 11: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 12: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 13: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 14: Karol Ostrovsky,K.V.S.Prasad,and Walid Taha. Towards primitive higher order calculus of broadcasting systems (extended version).URL: http://www.cs.chalmers.se/.karol/Papers/,March 2001.
• 15: K.V.S.Prasad.Status report on ongoing work: Higher order broadcasting systems and reasoning about broadcasts.Unpublished manuscript, September 1994.
• 16: K. V. S. Prasad, A calculus of broadcasting systems, Science of Computer Programming, v.25 n.2-3, p.285-327, Dec. 1995
• 17: K.V.S.Prasad.Broadcast calculus interpreted in CCSupto bisimulation.In EXPRESS '01:8th International Workshop on Expressiveness in Concurrency ,Electronic Notes in Theoretical Computer Science.Elsevier,2001.
• 18: Davide Sangiorgi.Expressing Mobility in Process Algebras:First-Order and Higher-Order Paradigms. PhD thesis CST. 99. 93, Department of Computer Science, University of Edinburgh, 1992.
• 19: Bent Thomsen.Plain CHOCS:A second generation calculus for higher order processes.Acta Informatica, 30(1):1--59, January 1993.
• 20: David N.Turner. The Polymorphic Pi-Calculus: Theory and Implementation .PhD thesis CST .126 .96, Dept.of Computer Science,University of Edinburgh, 1996.(also published as ECS-LFCS-96-345).

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.0 General

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.0 General
  D.3 PROGRAMMING LANGUAGES
      D.3.0 General

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Design, Languages, Theory, Verification

Keywords:
broadcasting, calculi, concurrency, ethernet, programming languages, semantics