ERC Consolidator Grant · 2022
Realizing the Promise of Higher-Order SMT and Superposition for Interactive Verification
Proof assistants (also called interactive theorem provers) have a long history of being very tedious to use. The situation has improved markedly in the past decade with the integration of first-order automatic theorem provers as backends. And recently, there have been exciting developments for more expressive logics, with the emergence of automatic provers based on optimized higher-order calculi. The Nekoka project's aim is to make higher-order SMT and λ-superposition a perfect fit for logical problems emerging from the verification of software and mathematics. We will start by extending higher-order SMT and λ-superposition and implementing them in automatic provers to provide push-button…
From the public funding record at EU CORDIS. Describes the funded project, not the reviews below.