SHF: Small: Lambda Encodings Reborn

SHF：小型：Lambda 编码重生

• 批准号: 1524519
• 负责人: Aaron Stump
• 金额: $ 46.89万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-08-01 至 2020-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1524519&HistoricalAwards=false
• 关键词: SHF; Small; Lambda; Encodings; Reborn

Proof assistants are software tools that assist users in developing formal proofs of theorems. Proof assistants are now widely used to verify large software systems. Hence a more trustworthy proof assistant could have significant impact on high assurance software. An important issue in the design of proof assistants is how to ensure they are logically sound. This project investigates a new foundation for proof assistants, based on a method of representing data using only functions which is known as lambda encodings. Lambda encodings are important for proof assistants because they eliminate the need for a datatype subsystem. Such subsystems are complicated, and increase the difficulty of ensuring logical soundness of the proof assistant. There are several technical problems in using lambda encoding for this purpose, including the fact that induction principles could not be derived using them. This project develops new solutions to these problems, that enables the use of lambda encodings as a viable foundation for proof assistants. These new methods will be integrated into a new proof assistant, called Cedille, which has a simpler foundation than other similar tools, and increases its trustworthiness.

证明助手是帮助用户开发定理的形式证明的软件工具。证明助手现在被广泛用于验证大型软件系统。因此，一个更值得信赖的证明助手可能会对高保证软件产生重大影响。证明助理设计中的一个重要问题是如何确保它们在逻辑上是正确的。该项目研究了证明助手的新基础，基于仅使用称为lambda编码的函数表示数据的方法。 Lambda编码对于证明助手很重要，因为它们消除了对数据类型子系统的需求。 这样的子系统是复杂的，并且增加了确保证明辅助的逻辑可靠性的难度。 使用lambda编码有几个技术问题，包括使用它们不能导出归纳原理的事实。 该项目为这些问题开发了新的解决方案，使lambda编码成为证明助手的可行基础。这些新方法将集成到一个名为Cedille的新证明助手中，该助手比其他类似工具具有更简单的基础，并提高了其可信度。