SHF: Small: Lambda Encodings Reborn

University Of Iowa, Iowa City IA

Investigators

Abstract

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.