论文标题
基于证明助手的核心Erlang的形式化
A Proof Assistant Based Formalisation of Core Erlang
论文作者
论文摘要
我们的研究是一个更广泛的项目的一部分，该项目旨在调查和推理基于计划的ERLANG计划的源代码转换的正确性。为了正式理解编程语言的定义以及使用它构建的软件，我们需要对该语言进行数学上严格的描述。 在本文中，我们介绍了基于证明的Erlang子集的形式化，旨在作为证明重构正确的基础。在讨论了我们如何从相关工作中重新使用概念之后，我们展示了正式描述的语法和语义，包括所涉及的抽象（例如关闭）。我们还提出了形式化（例如确定论）的基本特性及其机器检查的证明。最后，我们证明了一些简单的重构策略的正确性。
Our research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language. In this paper, we present our proof-assistant-based formalisation of a subset of Erlang, intended to serve as a base for proving refactorings correct. After discussing how we reused concepts from related work, we show the syntax and semantics of our formal description, including the abstractions involved (e.g. closures). We also present essential properties of the formalisation (e.g. determinism) along with their machine-checked proofs. Finally, we prove the correctness of some simple refactoring strategies.
