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.