A verified compiler for an impure functional language
A verified compiler for an impure functional language
复制标题
用于非纯函数语言的经过验证的编译器
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. Chlipala
中科院分区：
文献类型：
--
作者：
A. Chlipala
我们提出了一个经过验证的编译器，一个理想化的汇编语言从一个小的，无类型的函数式语言与可变的引用和异常。编译器是在Coq证明助手中编程的，并且具有关于源语言和目标语言的大步操作语义的完全正确性证明。编译是分阶段的，包括标准阶段，如转换为延续传递风格和闭包转换，以及常见的子表达式消除优化。在这项工作中，我们的重点是发现和使用技术，使我们的证明易于工程和维护。虽然大多数使用证明助手的编程语言工作使用非常手动的证明风格，但我们所有的证明都是在Coq的策略语言中实现的自适应程序，因此可以在添加新语言功能时重复使用未更改的证明。
在本文中，我们特别关注的阶段，重新安排的语法结构与嵌套变量绑定器的编译。在过去的编译器验证项目中，这方面一直是一个关键的挑战领域，在绑定器相关引理的陈述和证明方面花费的精力比标准的文件和纸张证明要多得多。我们将展示如何利用参数高阶抽象语法的表示技术，以避免需要证明任何常见的引理绑定操作，往往导致证明，实际上是短于他们的纸和纸的类似物。我们的策略是基于一种新的方法来编码操作语义，代表所有的关注替代Meta语言，而不使用功能不兼容的通用类型理论，如Coq的逻辑。
We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in the Coq proof assistant and has a proof of total correctness with respect to big-step operational semantics for the source and target languages. Compilation is staged and includes standard phases like translation to continuation-passing style and closure conversion, as well as a common subexpression elimination optimization. In this work, our focus has been on discovering and using techniques that make our proofs easy to engineer and maintain. While most programming language work with proof assistants uses very manual proof styles, all of our proofs are implemented as adaptive programs in Coq's tactic language, making it possible to reuse proofs unchanged as new language features are added.
In this paper, we focus especially on phases of compilation that rearrange the structure of syntax with nested variable binders. That aspect has been a key challenge area in past compiler verification projects, with much more effort expended in the statement and proof of binder-related lemmas than is found in standard pencil-and-paper proofs. We show how to exploit the representation technique of parametric higher-order abstract syntax to avoid the need to prove any of the usual lemmas about binder manipulation, often leading to proofs that are actually shorter than their pencil-and-paper analogues. Our strategy is based on a new approach to encoding operational semantics which delegates all concerns about substitution to the meta language, without using features incompatible with general-purpose type theories like Coq's logic.