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.

翻译：为了对编程语言描述的程序行为进行推理，需要为该语言提供数学上严谨的定义。本文基于我们先前对Core Erlang（Erlang的子集）顺序子语言的形式化工作，提出了一种并发Core Erlang的机器验证形式化方法。我们定义了一种模块化帧栈语义，展示了如何通过该语义执行程序求值，并证明了若干性质（例如确定性、合流性）。最后，我们基于双模拟定义了程序等价性，并证明了无副作用求值是一种双模拟。本研究是更广泛项目的一部分，旨在验证重构的正确性，以确保特定程序代码变换能够保持程序行为。