SHF: Small: Lambda Encodings Reborn

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

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.