Semantics for communication primitives in a polymorphic language

Atsushi Ohori, Kazuhiko Kato

Research output: Chapter in Book/Report/Conference proceedingConference contribution

26 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationConference Record of the Annual ACM Symposium on Principles of Programming Languages
PublisherPubl by ACM
Pages99-112
Number of pages14
ISBN (Print)0897915607
Publication statusPublished - 1993 Jan 1
Externally publishedYes
Event20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Charleston, SC, USA
Duration: 1993 Jan 101993 Jan 13

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CityCharleston, SC, USA
Period93/1/1093/1/13

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Semantics for communication primitives in a polymorphic language'. Together they form a unique fingerprint.

Cite this