SHF: Small: Mechanized reasoning for functional programs

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

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.