2016-09-06
A formal, resource consumption-preserving translation of actors to Haskell
Publication
Publication
Presented at the
International Symposium on Logic-Based Program Synthesis and Transformation (September 2016), Edinburgh, UK
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.
| Additional Metadata | |
|---|---|
| doi.org/10.1007/978-3-319-63139-4_2 | |
| International Symposium on Logic-Based Program Synthesis and Transformation | |
| Organisation | 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 |
|
