A Formalisation of Core Erlang, a Concurrent Actor Language

Keywords: formal semantics, formal verification, concurrency, actor model, program equivalence, bisimulation, Erlang, Core Erlang, Coq

Abstract

In order to reason about the behaviour of programs described in a programming language, a mathematically rigorous definition of that language is needed. In this paper, we present a machine-checked formalisation of concurrent Core Erlang (a subset of Erlang) based on our previous formalisations of its sequential sublanguage. We define a modular, frame stack semantics, show how program evaluation is carried out with it, and prove a number of properties (e.g. determinism, confluence). Finally, we define program equivalence based on bisimulations and prove that side-effect-free evaluation is a bisimulation. This research is part of a wider project that aims to verify refactorings to prove that particular program code transformations preserve program behaviour.

Downloads

Download data is not yet available.
Published
2024-03-04
How to Cite
Bereczky, P., Horpácsi, D., & Thompson, S. (2024). A Formalisation of Core Erlang, a Concurrent Actor Language. Acta Cybernetica, 26(3), 373-404. https://doi.org/10.14232/actacyb.298977
Section
Special Issue of the 13th Conference of PhD Students in Computer Science