Formal Verification of Compiler Algorithms

由于编译器几乎是每个计算机系统的可信组件，因此对其正确性拥有可信的证明是很重要的。最近发展了一种用高阶抽象汇编语言证明编译器正确性的新方法。这个项目是研究如何将这种证明扩展到更现实的编译器。对证明过程的机械支持将通过对人类证明人的工作提供独立的验证，从而使最终的证明更可信。这个项目的三个主要活动领域包括：(1)使用机械定理证明器来支持编译器正确性证明，(2)将这种证明扩展到优化编译器，以及(3)合作开发用于方案的经验证的编译器。

Because compilers are trusted components of almost every computer system, it is important to have trustworthy proofs of their correctness. A new method of proving compilers correct using higher- order abstract assembly language has been developed recently. This project is to study how to extend such proofs to more realistic compilers. Mechanical support for the proof process will allow the resulting proofs to be more trustworthy by supplying independent verification of the human prover's work. Three main areas of activities in this project include: (1) the use of mechanical theorem- provers to support compiler correctness proofs, (2) the extension of such proofs to optimizing compilers, and (3) a cooperative development of a verified compiler for Scheme.