CAREER: Specification and Verification of Compiler Algorithms

这个CAREER项目的研究目标是对支持编程语言实现的算法进行形式化规范和验证。这样的正式系统可以帮助新语言的开发和这些语言的有效实现。这种支持来自对算法的验证（这增加了对编译器正确性的信心）和对正式规范所允许的编译技术的改进理解。最近的工作集中在使用逻辑框架和机械化证明助手来指定表示编译方面的演绎系统，并验证这些规范的正确性。本研究项目通过考虑当前编译器中发现的先进的，最先进的算法，形式化这些算法的理论，并验证这些算法的正确性，扩展了这些结果。需要解决的一个特定问题领域涉及闭包转换算法和“空间安全复杂性”的概念。“该项目的一个重要方面是扩展机械化证明助手的使用，以支持复杂流程分析和程序优化的验证。该教育计划的目标是为本科阶段的编程语言学习提供一个一般但严格的介绍，并将在本科和研究生阶段介绍最近出现的逻辑和计算领域，该领域研究构造逻辑和类型化lambda演算之间的关系。虽然这通常被认为是高级材料，不适合本科生，但它可以为学生提供。

The research goal of this CAREER project is the formal specification and verification of algorithms that support the implementation of programming languages. Such formal systems can aid the development of new languages and efficient implementation of these languages. This support arises from both the verification of algorithms, which increases confidence in the correctness of a compiler, and from the improved understanding of compilation techniques allowed by formal specification. Recent work has focused on using logical frameworks and mechanized proof assistants to specify deductive systems representing aspects of compilation and to verify the correctness of these specifications. This research project extends these results by considering advanced, state-of-the-art algorithms found in current compilers, formalizing theories for these algorithms, and verifying the correctness of these algorithms. One specific problem area to be addressed involves closure conversion algorithms and the concept of `safe-for-space complexity.` An important aspect of this project is extending the use of mechanized proof assistants to support the verification of complex flow analyses and optimizations of programs. The goal of the education plan is to provide both a general, but rigorous, introduction to the study of programming languages at the undergraduate level and would introduce, at both the undergraduate and graduate level, the recently emerging field of logic and computation which studies the relationship between constructive logics and typed lambda calculi. Although this is typically considered advanced material and not suitable for undergraduates, it can be made accessible to students.