SHF: Small: Mechanized reasoning for functional programs

这个项目调查了交互式证明助手用于推理用函数式编程语言编写的程序的属性，特别关注用Haskell编程语言编写的代码，并使用Coq证明助手进行验证。这个项目的结果将增加我们对机械推理的理解，以及它在通过规范识别和错误检测在各种软件系统的开发中的作用。换句话说，开发团队应该能够使用证明助手来发现应适用于代码库的属性和不变量的正式描述，并识别违反这些属性的代码库部分。此外，该项目还开发了可在未来开发中使用的翻译库、其规范和属性的语料库。该项目围绕着一个名为hs-to-coq的验证工具的开发、扩展和使用展开，该工具可以半自动地将未经修改的Haskell源代码翻译成Coq验证助手的语言。该项目将hs-to-coq扩展到coq，以便它可以应用于有效的代码，这些代码使用一元操作来表达副作用，如输入/输出和其他有状态计算。该项目考虑使用并发、可变状态、异常或操作系统调用的Haskell代码。为此，项目成员调查了一元和代数结构的使用，如交互树、自由单体和效果处理程序，在原始Haskell代码中和在Coq中支持有效代码建模。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

This project investigates the usage of interactive proof assistants for reasoning about the properties of programs written in functional programming languages, with the specific focus on code written in the Haskell programming language and verified using the Coq proof assistant. Results from this project will increase our understanding of mechanical reasoning and its role in the development of a wide variety of software systems through specification identification and bug detection. In other words, development teams should be able to use proof assistants to discover a formal description of the properties and invariants that should hold for a code base and to identify parts of the code base that violate those properties. Additionally, the project develops a corpus of translated libraries, their specifications, and properties that may be used in future developments.The project centers around the development, extension and use of a verification tool, called hs-to-coq that semi-automatically translates unmodified Haskell source code to the language of the Coq proof assistant. This project extends hs-to-coq so that it may be applied to effectful code which express side effects like input/output and other stateful computations using monadic actions. The project considers Haskell code that makes use of concurrency, mutable state, exceptions, or operating system calls. To this end, project members investigate the use of monadic and algebraic structures, such as interaction trees, free monads and effect handlers, both in the original Haskell code and in support of modeling effectful code in Coq.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.