SHF: Small: Mechanized reasoning for functional programs

SHF：小型：函数式程序的机械化推理

基本信息

批准号：
2006535
负责人：
Stephanie Weirich
金额：
$ 45万
依托单位：
University of Pennsylvania
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-10-01 至 2024-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2006535&HistoricalAwards=false
关键词：
SHF Small Mechanized reasoning functional

项目摘要

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.

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