Professor Aaron Stump is the Principle Investigator for a grant recently awarded by the NSF.

The project, entitled "SHF: Small: Lambda Encodings Reborn" develops new solutions to technical problems in using lambda encoding as a viable foundation for proof assistants — software tools that assist users in developing formal proofs of theorems. 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; which could have significant impact on high assurance software.

This three-year project has been awarded $468,938.

Unabridged award abstract may be found here.