A Formal, Resource Consumption-Preserving Translation of Actors to Haskell
Elvira Albert, Nikolaos Bezirgiannis, Frank de Boer, Enrique, Martin-Martin

TL;DR
This paper introduces a formal translation from an actor-based language with cooperative scheduling to Haskell, ensuring correctness and resource consumption preservation, validated through formal semantics and simulation relations.
Contribution
It provides the first formal, resource-preserving translation from actor-based models to Haskell with proven correctness using simulation relations.
Findings
The translation is proven correct with respect to formal semantics.
Resource consumption is preserved during translation.
The approach is validated through formal proofs of equivalence.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Distributed systems and fault tolerance · Parallel Computing and Optimization Techniques
