CAREER: Specification and Verification of Compiler Algorithms

职业：编译器算法的规范和验证

• 批准号: 9502356
• 负责人: John Hannan
• 金额: $ 13万
• 依托单位: Pennsylvania State Univ University Park
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-05-01 至 1998-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9502356&HistoricalAwards=false
• 关键词: CAREER; Specification; Verification; Compiler; Algorithms

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.

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