paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Compiling a 50-year journey

编译的五十年历程
JFP vol.272017匹配度 2/10 · 论文属于经典的程序验证与编译器正确性推导，虽然与形式化验证相关，但未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向，且没有工业落地或问题驱动 benchmark 内容。引用 7 inbox
GRAHAM HUTTON, PATRICK BAHR
编译与代码生成程序验证
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话：以等式推理从正确性规约直接推导出算术表达式编译器，重访编译器验证的起源。

五十年前，John McCarthy 和 James Painter 发表了首篇编译器验证论文，展示了如何形式化证明一个将算术表达式翻译为寄存器机代码的编译器的正确性。本文在现代语境下重新审视这一经典例子，说明如今可以借助简单的等式推理技术，直接从编译器正确性规约出发计算得到该编译器，而不再仅仅是对已写出的编译器进行事后验证。这一工作以现代视角串联起编译器验证五十年的发展，并展示了规约驱动、计算式构造编译器的可行路径。

问题
如何以更简洁、可计算的方式构造并保证算术表达式到寄存器机代码的编译器正确性。
方法
在现代语境下重访 McCarthy 与 Painter 的编译器验证例子，使用简单的等式推理技术，从编译器正确性规约出发直接计算得到编译器。
评估
通过形式化推导与经典案例重访，展示该编译器可由其正确性规约计算得到，而非仅进行事后正确性证明。
原文摘要（Abstract）

Abstract Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this article, we revisit this example in a modern context, and show how such a compiler can now be calculated directly from a specification of its correctness using simple equational reasoning techniques.

链接与引用

DOI 原文 · PDF（开放获取） · DBLP

BibTeX 
@article{HuttonB17,
  title = {Compiling a 50-year journey},
  author = {GRAHAM HUTTON and PATRICK BAHR},
  journal = {Journal of Functional Programming},
  volume = {27},
  year = {2017},
  doi = {10.1017/s0956796817000120}
}