This is a project to increase the capabilities of Logical Programming Environments (LPE's). These systems provide formal support to the programming and software evolution process, including advanced type checking and formal verification of code. They comprise a programming language, a specification language, a programming logic and a theorem prover.
The core innovation is to link three theorem provers, HOL, Nuprl and PVS to an LPE. The first new capability enabled is sharing libraries of basic mathematical facts. This is a technically challenging task, but accomplishing it advances many of the goals, indeed it appears to be essential to achieving some of these goals. Moreover accomplishing it will enlarge the formal design space available for managing complex software.
The second new capability is that combinations of tools, provers, decision procedure and model checkers can cooperate on system verifications. Moreover, a new concept of a multi-logic proof can be explored, and we propose new ways of guaranteeing the soundness of these extended proofs. In particular we propose to provide logic-based accounting mechanisms to inform users of formal tools exactly what assumptions they depend on and what level of verification has been achieved for them. Additionally we will provide a means to harden the decision procedures and model checkers that are now often operated without high assurance, as ordinary pieces of software.
The Logical Programming Environment will be based on type theory which has proven itself so well over the past two decades as a unifying semantic framework, providing concepts that have been successful in modeling actual software systems as well as in providing the semantics for a wide variety of programming logics. Moreover, implementations of type theories have supported large constellations of formal tools proven to be useful in analyzing and reasoning about such software. The type theory provides a natural basis for tools to interoperate.
By building on Logical Programming Environments, we will improve the methods to link running code to its specifications and to link formal models of what the code is doing. This involves opening the tools used to correctly transform programs and also improving the link between code and specifications that our group at Cornell pioneered, namely the extraction of programs from proofs that programming tasks are tractably solvable. Finally we want to explore some very new ideas for treating formal theories as software systems, a generalization of the notion that proofs are like programs.
The results we produce will enable researchers to eventually concentrate an unprecedented amount of formal power on the task of building more reliable and secure software and to demonstrate new capabilities for controlling complex software. We will demonstrate this on verifications we are now doing under DARPA contract on distributed computing middleware.