A Formal, Resource Consumption-Preserving Translation of Actors to Haskell

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.