Abstract
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.
Cite
CITATION STYLE
Albert, E., Bezirgiannis, N., de Boer, F., & Martin-Martin, E. (2017). A formal, resource consumption-preserving translation of actors to Haskell. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10184 LNCS, pp. 21–37). Springer Verlag. https://doi.org/10.1007/978-3-319-63139-4_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
