SHF: Medium: Collaborative Research: Principled Optimizing Compilation of Dependently Typed Languages

SHF：媒介：协作研究：依赖类型语言的原则优化编译

• 批准号: 1407790
• 负责人: John Morrisett
• 金额: $ 60万
• 依托单位: Harvard University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-07-01 至 2015-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1407790&HistoricalAwards=false
• 关键词: SHF; Medium; Collaborative; Research; Principled

Title: SHF: Medium: Collaborative Research: Principled Optimizing Compilation of Dependently Typed LanguagesThe project focuses on a form of software engineering with program verification: writing programs with logical, machine-checkable proofs of correctness, reliability, or security. Such proofs can be done for programs written in conventional programming languages, but the "proof theory" of these languages is complex and difficult, which makes verification time-consuming and expensive. New, "dependently typed" programming languages use principles of functional programming and advanced type systems to achieve a smoother and cleaner proof theory, so that verifying the correctness and safety of software (written in these new languages) is much easier. In this project, the research is to build compilers for these new languages that are efficient and are verified correct.The intellectual merits are in the challenges and opportunities that occur in dependently typed, purely functional contexts, such as the Coq proof assistant. The exciting opportunities that arise only in this context are the ability to choose evaluation order for any sub-term (since Coq's language is pure and total), the ability to open a compiler to user-specified (and certified) rewrite rules that support application-specific optimization, and the ability of programmers to use the Calculus of Inductive Constructions (CiC) proof theory of Coq to verify their programs. The challenges we face, unique to this setting, include the need to determine and erase those terms that are computationally irrelevant. A major foundational challenge is attempting to preserve types (and hence proofs) as we perform lowering transformations, such as conversion to continuation-passing style (CPS) or static single assignment (SSA). Our strategy is to use type and proof-preserving compilation where possible, and where not, to prove a simulation-based notion of correctness. The broader impacts will include (1) pedagogical materials on verified functional programming in Coq; (2) training of graduate students; and (3) improvements in software engineering practice, in enabling practical verified functional programming.

职务名称：SHF：中等：合作研究：该项目侧重于软件工程与程序验证的一种形式：编写具有逻辑，机器可检查的正确性，可靠性或安全性证明的程序。 这样的证明可以对用传统编程语言编写的程序进行，但是这些语言的“证明理论”复杂而困难，这使得验证耗时且昂贵。 新的“依赖类型”编程语言使用函数式编程和高级类型系统的原则来实现更平滑和更清晰的证明理论，因此验证软件（用这些新语言编写）的正确性和安全性要容易得多。 在这个项目中，我们的研究是为这些新的语言构建编译器，这些编译器是高效的，并且被验证是正确的。智力上的优点是在依赖类型的纯函数式上下文中出现的挑战和机遇，例如Coq证明助手。 只有在这种情况下才会出现令人兴奋的机会是为任何子项选择求值顺序的能力（因为Coq的语言是纯的和全面的），打开编译器以支持特定于应用程序的优化的用户指定（和认证）重写规则的能力，以及程序员使用Coq的归纳构造演算（CiC）证明理论来验证他们的程序的能力。 我们所面临的挑战，独特的这种设置，包括需要确定和删除这些条款是计算无关。 一个主要的基本挑战是在我们执行降低转换时试图保留类型（以及证明），例如转换为延续传递风格（CPS）或静态单一赋值（SSA）。 我们的策略是在可能的情况下使用类型和证明保留编译，而在不可能的情况下，证明基于模拟的正确性概念。 更广泛的影响将包括：（1）关于Coq验证函数编程的教学材料;（2）研究生培训;（3）改进软件工程实践，实现实际验证函数编程。