We present a formal translation of an actor-based language with cooperative scheduling to the functional language Haskell. The translation is proven correct with respect to a formal semantics of the source language and a high-level operational semantics of the target, i.e. a subset of Haskell. The main correctness theorem is expressed in terms of a simulation relation between the operational semantics of actor programs and their translation. This allows us to then prove that the resource consumption is preserved over this translation, as we establish an equivalence of the cost of the original and Haskell-translated execution traces.

International Symposium on Logic-Based Program Synthesis and Transformation
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Albert, E., Bezirgiannis, N., de Boer, F., & Martin-Martin, E. (2016). A formal, resource consumption-preserving translation of actors to Haskell. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 21–37). doi:10.1007/978-3-319-63139-4_2