We present a small-step, frame stack style, semantics for sequential Core Erlang, a dynamically typed, impure functional programming language. The semantics and the properties that we prove are machine-checked with the Coq proof assistant. We improve on previous work by including exceptions and exception handling, as well as built-in data types and functions. Based on the semantics, we define multiple concepts of program equivalence (contextual, CIU equivalence, and equivalence based on logical relations) and prove that the definitions are all equivalent. Using this we are able to give a correctness criterion for refactorings by means of contextually equivalent symbolic expression pairs, which is one of the main motivations of this work.

翻译：我们提出了一种面向序列化核心Erlang（一种动态类型、不纯的函数式编程语言）的小步帧栈语义。该语义及其所证明的性质均通过Coq证明助手进行机器验证。相较于先前工作，我们改进了对异常及其处理机制、内置数据类型与函数的支持。基于该语义，我们定义了多种程序等价性概念（上下文等价、CIU等价及基于逻辑关系的等价性），并证明这些定义彼此等价。借此，我们能够通过上下文等价的符号表达式对给出重构的正确性准则——这也是本研究的主要动机之一。