FMitF: Track II: Refinement Types in the Haskell Ecosystem

FMITF：轨道 II：Haskell 生态系统中的细化类型

• 批准号: 1917854
• 负责人: Ranjit Jhala
• 金额: $ 10万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1917854&HistoricalAwards=false
• 关键词: FMitF; Track; II; Refinement; Types

Formal methods for ensuring the reliability of software will only become ubiquitous if they can be seamlessly integrated within widely used language ecosystems. The Liquid Haskell (LH) system integrates verification within the Haskell programming language, by allowing developers to specify correctness requirements as contracts extending Haskell's types. LH can then automatically verify these contracts at compile-time ensuring the deployed program will always execute according to its specification. This project's novelties are in new methods to integrate LH within the Glasgow Haskell Compiler (GHC) toolchain. Consequently, the project's impacts will be to enable tight integration within the engineering workflow used in industry making it possible to run LH on large, industrial code bases.This project will build on GHC's recently added plugins and annotations mechanisms to integrate refinement types within the compiler. This integration will allow LH to reuse GHC's module system to allow programmers to publish specifications for their libraries that can be reused by clients of those modules, and to support incremental verification that is essential for scaling verification to industrial sized code bases. As a result, the project will yield a tool that is tightly integrated within a widely used, industrial strength compiler, enabling engineers to utilize decades worth of formal methods research to eliminate hard-to-find correctness bugs from deployed systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

确保软件可靠性的正式方法只有能够无缝集成到广泛使用的语言生态系统中才会变得普遍。 Liquid Haskell (LH) 系统将验证集成到 Haskell 编程语言中，允许开发人员将正确性要求指定为扩展 Haskell 类型的合约。然后，LH 可以在编译时自动验证这些合约，确保部署的程序始终按照其规范执行。该项目的新颖之处在于将 LH 集成到 Glasgow Haskell 编译器 (GHC) 工具链中的新方法。因此，该项目的影响将是实现工业中使用的工程工作流程中的紧密集成，从而可以在大型工业代码库上运行 LH。该项目将建立在 GHC 最近添加的插件和注释机制的基础上，以在编译器中集成细化类型。这种集成将允许 LH 重用 GHC 的模块系统，以允许程序员发布可供这些模块的客户端重用的库的规范，并支持增量验证，这对于将验证扩展到工业规模的代码库至关重要。因此，该项目将产生一个与广泛使用的工业强度编译器紧密集成的工具，使工程师能够利用数十年的形式方法研究来消除部署系统中难以发现的正确性错误。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。