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.