Semantics for communication primitives in a polymorphic language

ABSTRACT

We propose a method to extend an ML-style polymorphic language with transparent communication primitives, and give their precise operational semantics. These primitives allow any polymorphic programs definable in ML to be used remotely in a manner completely transparent to the programmer. Furthermore, communicating programs may be based on different architecture and use different data representations. We define a polymorphic functional calculus with transparent communication primitives, which we call dML, as an extension of Damas and Milner's proof system for ML. We then develop an algorithm to translate dML to a “core” language containing only low-level communication primitives that are readily implementable in most of distributed environments. To establish the type safety of communicating programs, we define an operational semantics of the core language and prove that the polymorphic type system of dML is sound with respect to the operational semantics of the translated terms of the core language.

REFERENCES

• ABC+83: M.P. Atldnson, P.J. Bailey, K.J. Chisholm, W.P. Cockshott, and R. Morrison. An approach to persistent programming. Computer Journal, 26(4), November 1983.
• ACPP91: Martín Abadi , Luca Cardelli , Benjamin Pierce , Gordon Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.237-268, April 1991 [doi>10.1145/103135.103138]
• ACPR92: M. Abadi, L. Cardelli, B. Pierce, and D. R~my. Dynamic typing in polymorphie languages, in A CM SIGPLAN Workshop on ML and its Applications, 1992.
• BMT92: Dave Berry , Robin Milner , David N. Turner, A semantics for ML concurrency primitives, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-129, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143191]
• BN84: Andrew D. Birrell , Bruce Jay Nelson, Implementing remote procedure calls, ACM Transactions on Computer Systems (TOCS), v.2 n.1, p.39-59, February 1984 [doi>10.1145/2080.357392]
• BO92: Peter Buneman , Atsushi Ohori, Polymorphism and type inference in database programming, ACM Transactions on Database Systems (TODS), v.21 n.1, p.30-76, March 1996 [doi>10.1145/227604.227609]
• BST89: Henri E. Bal , Jennifer G. Steiner , Andrew S. Tanenbaum, Programming languages for distributed computing systems, ACM Computing Surveys (CSUR), v.21 n.3, p.261-322, Sep. 1989 [doi>10.1145/72551.72552]
• CK92: R. Cooper and C. Krumvioda. Distributed programming with asynchronous ordered channels in distributed ML. In Proceedings of the A CM SIGPLAN Workshop on ML and its Applications, June 1992.
• CW85: Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
• DM82: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• HL82: Maurice P. Herlihy , Barbara Liskov, A Value Transmission Method for Abstract Data Types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.4, p.527-551, Oct. 1982 [doi>10.1145/69622.357182]
• HS87: Roger Hayes , Richard D. Schlichting, Facilitating mixed language programming in distributed systems, IEEE Transactions on Software Engineering, v.13 n.12, p.1254-1264, December 1, 1987 [doi>10.1109/TSE.1987.232879]
• JR86: Michael B. Jones , Richard F. Rashid, Mach and Matchmaker: kernel and language support for object-oriented distributed systems, Conference proceedings on Object-oriented programming systems, languages and applications, p.67-77, September 29-October 02, 1986, Portland, Oregon, United States
• KO92: K. Kato and A Ohod. An approach to multilanguage persistent type system. In Proc. Hawaii International Confernece on System Science, pages 810-819, 1992.
• LBG+87: B. Liskov, T. Bloom, D. Gifford, R. Scheifler, and W. Weihl. Communication in the Mercury system. Programming Methodology Group Memo 59, MIT, 1987.
• Ler92: Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
• LM91: Xavier Leroy , Michel Mauny, Dynamics in ML, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.406-426, June 1991, Cambridge, Massachusetts, United States
• LMO92: Gary Lindstrom , Jan Maluszynski , Takeshi Ogi, Our LIPS Are Sealed: Interfacing Functional and Logic Programming Systems, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.428-442, August 26-28, 1992
• Mac88: D. MacQueen. References and weak polymorphism. Note in Standard ML of New Jersey Distribution Package, 1988.
• MH88: J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
• Mil78: R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.
• MP88: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• MTH90: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• Oho92: Atsushi Ohori, A compilation method for ML-style polymorphic record calculi, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-165, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143200]
• Rep91: John H. Reppy, CML: A higher concurrent language, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.293-305, June 24-28, 1991, Toronto, Ontario, Canada
• Tof88: M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Department of Computer Science, University of Edinburgh, 1988.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types; Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Design, Languages, Theory