Description of the Project

The world is engaged in a grand scientific and technological enterprise to build a global information resource. It will include vast digital collections of scientific information. Creating this global resource will be one of the great achievements of information technology. The research of our group at Cornell, Cal Tech and Wyoming on applied logic, formal methods and automated reasoning will make the emerging information resource more capable -- first by providing a basis for semantic processing of information and for a logical accounting of its structure, essential to creating knowledge, and second by including among the resources an interactive digital library of formal computational mathematics. Such a library will bring into being a "formal forum" that will connect experts and practitioners together in building reliable software systems, educating the information technology work force, empowering the lay scientist, and in nucleating the creation of a broader open library of formally grounded knowledge. Our contributions to this enterprise will impact all these uses and will make the global information resource especially valuable in designing reliable software systems.

Our research group has devoted considerable effort over the years to demonstrate the value of constructive methods, both in foundational theory and in significant applications. We have built systems that we and others have used to create large amounts of formal content and to support the design and verification of software. Currently we develop and use two different systems which interact; to connect them we have been led to create advanced formal information management tools as part of our logical library. We know some of the problems involved in scaling these tools to support the emerging global digital library of formal content and to support collaborative theory building and reliable software construction. One of the most critical challenges is finding methods to track dependencies among library objects in an environment that allows justifications of inference steps to include programs (called tactics). Another key challenge is devising accounting mechanisms that allow different theorem provers to share results consistently and allow users to merge results developed independently. A further issue is implementing operations that soundly transform entire algorithmic theories and translate among them.

Creating formal algorithmic content requires systems that are very expressive and very fast. We explore both aspects which leads us to problems that have been unsolved for many years, such as how to implement a practical general reflection mechanism in an open system and how to reason about computational complexity in formal theories. For speed we are led to building concurrent interactive provers. For more expressiveness, we are led to concepts and tools for proving and programming "in the large." Our research agenda on these topics is critical to building digital libraries of formal algorithmic knowledge which in turn will significantly enhance the nation's ability to design, build and maintain reliable software systems.