FMitF: Track II: Refinement Types in the Haskell Ecosystem

点击翻译按钮获取中文摘要

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.