A Formalisation of Core Erlang, a Concurrent Actor Language.
CoRR(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要