论文标题
程序等效性，具有未经递归功能
Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions
论文作者
论文摘要
我们的目标是推理Erlang程序的保护性转换的正确性。行为保存的特征在于语义等效性。基于我们现有的核心Erlang语义，我们研究了适当的等效关系的潜在定义。特别是，我们将许多现有表达等效性的方法调整为一种简单的功能编程语言，该语言具有顺序核心Erlang的主要特征。然后，我们检查等效关系的属性，并正式建立它们之间的联系。本文中介绍的结果，包括所有定理及其证明，已使用COQ证明助手进行了检查。
We aim to reason about the correctness of behaviour-preserving transformations of Erlang programs. Behaviour preservation is characterised by semantic equivalence. Based upon our existing formal semantics for Core Erlang, we investigate potential definitions of suitable equivalence relations. In particular we adapt a number of existing approaches of expression equivalence to a simple functional programming language that carries the main features of sequential Core Erlang; we then examine the properties of the equivalence relations and formally establish connections between them. The results presented in this paper, including all theorems and their proofs, have been machine checked using the Coq proof assistant.
