Back to Search
Start Over
A Formalisation of Core Erlang, a Concurrent Actor Language.
- Source :
- Acta Cybernetica; 2024, Vol. 26 Issue 3, p373-404, 32p
- Publication Year :
- 2024
-
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. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 0324721X
- Volume :
- 26
- Issue :
- 3
- Database :
- Complementary Index
- Journal :
- Acta Cybernetica
- Publication Type :
- Academic Journal
- Accession number :
- 178843706
- Full Text :
- https://doi.org/10.14232/actacyb.298977