A formalisation of Core Erlang, a concurrent actor language
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 it...
Elmentve itt :
| Szerzők: | |
|---|---|
| Dokumentumtípus: | Cikk |
| Megjelent: |
University of Szeged, Institute of Informatics
Szeged
2024
|
| Sorozat: | Acta cybernetica
26 No. 3 |
| Kulcsszavak: | Programozás, Programozási nyelv, Programverifikáció |
| Tárgyszavak: | |
| doi: | 10.14232/actacyb.298977 |
| Online Access: | http://acta.bibl.u-szeged.hu/86978 |
| Tartalmi kivonat: | 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. |
|---|---|
| Terjedelem/Fizikai jellemzők: | 373-404 |
| ISSN: | 2676-993X |