In this paper we present two actor languages: a high level User Language and a low level Kernel Language. The user language is object-oriented. Actors qua objects have methods and synchronization constraints which allow an object to control when a method can be invoked. The kernel language is an extension of a simple functional language with primitives for actor computation. Each of the languages is given a simple operational semantics via a labelled transition system, and an abstract interaction semantics derived from the computations of the transition system. The main result presented here is a translation from the user language to the kernel language and a proof that this mapping preserves the interaction semantics. This demonstrates that the basic actor primitives of the kernel are as expressive as those of the user language, although perhaps less convenient from a programmers point of view. The proof itself is of interest since it demonstrates a methodology based on abstract actor structures for proving correctness of transformations and translations of actor languages and more generally of concurrent object languages.
Keywords: actor language, interaction semantics, abstract actor structure, translation, correctness