FMitF: Track II: Refinement Types in the Haskell Ecosystem

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

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.