Bereczky Péter; Horpácsi Dániel; Thompson Simon: A formalisation of Core Erlang, a concurrent actor language. In: Acta cybernetica, (26) 3. pp. 373-404. (2024)
Előnézet |
Cikk, tanulmány, mű
cybernetica_026_numb_003_373-404.pdf Letöltés (729kB) | Előnézet |
Absztrakt (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.
| Mű típusa: | Cikk, tanulmány, mű |
|---|---|
| Befoglaló folyóirat/kiadvány címe: | Acta cybernetica |
| Dátum: | 2024 |
| Kötet: | 26 |
| Szám: | 3 |
| ISSN: | 2676-993X |
| Oldalak: | pp. 373-404 |
| Nyelv: | angol |
| Kiadó: | University of Szeged, Institute of Informatics |
| Kiadás helye: | Szeged |
| Befoglaló mű URL: | https://acta.bibl.u-szeged.hu/86904/ |
| DOI: | 10.14232/actacyb.298977 |
| Kulcsszavak: | Programozás, Programozási nyelv, Programverifikáció |
| Megjegyzések: | Bibliogr.: p. 402-404. ; összefoglalás angol nyelven |
| Szakterület: | 01. Természettudományok 01. Természettudományok > 01.02. Számítás- és információtudomány |
| Feltöltés dátuma: | 2025. ápr. 15. 15:18 |
| Utolsó módosítás: | 2025. ápr. 15. 15:18 |
| URI: | http://acta.bibl.u-szeged.hu/id/eprint/86978 |
 |
Tétel nézet |
