FMitF: Track II: Refinement Types in the Haskell Ecosystem

确保软件可靠性的正式方法只有在它们能够无缝地集成到广泛使用的语言生态系统中时才会变得无处不在。Liquid Haskell(LH)系统集成了Haskell编程语言中的验证，允许开发人员将正确性要求指定为扩展Haskell类型的合同。然后，lh可以在编译时自动验证这些契约，以确保部署的程序将始终根据其规范执行。该项目的创新之处在于采用了新的方法将lh集成到Glasgow Haskell编译器(GHC)工具链中。因此，该项目的影响将是实现在工业中使用的工程工作流中的紧密集成，使其能够在大型工业代码库上运行LH。该项目将建立在GHC最近添加的插件和注释机制的基础上，以将精化类型集成到编译器中。这一集成将允许LG重用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.