Introduction

The project is funded by a Department of Defense MURI (Multidisciplinary University Research Initiative program) grant announced and described in the following Broad Area Announcement (BAA):

DOD - Critical Infrastructure Protection and High Confidence, Adaptable Software Research Program of the University Research Initiative. The U.S. Department of Defense (DOD) announces an additional Fiscal Year 2001 competition of the University Research Initiative (URI). The URI is a DOD initiative to enhance universities' capabilities to perform science and engineering research and related education in science and engineering areas critical to national defense.

Topic Area #8: Digital Libraries for Constructive Mathematical Knowledge

Background: Software itself is fundamentally about algorithms. And, knowledge about algorithms is derived from discoveries in mathematical sciences that can be expressed constructively. The research community accepts discoveries as fact only after a lengthy process of review, validation, and acceptance, which has been remarkably effective. Consequentially, software assurance depends upon this understanding, trust, and experience in constructive mathematics and its expression. Systematically developing an infrastructure for this knowledge of algorithms -- as in a digital library -- would contribute to higher quality software, greater confidence in program construction, faster dissemination of knowledge globally, and deeper connections between mathematics and a science of programming, This development begins by codifying constructive mathematical knowledge using a view of computation as deduction and by engaging the research community in the pursuit of this national infrastructure.

Objective: To create a digital library of algorithms and constructive mathematics usable for program and software construction.

Research Concentration Areas: (1) Develop proof-checking and model checking for certifying proofs of the standard body of computationally related mathematics. (2) Catalog those principal mathematical concepts, together with their formal definitions, which are used in contemporary computing. (3) Investigate suitable base language and logic within which competing logics can be expressed and evaluated. (4) Provide automated assistance for routine aspects of developing libraries of formal theorems, proofs, algorithms, and their expressions as programs. (5) Investigate forms of assured interoperation for assembling, composing, specializing, and generalizing algorithmic knowledge. (6) Investigate reflection for coordination, interoperation, and dynamic adaptation. (7) Study issues of consistency and maintenance among libraries. (8) Address the human-computing aspects of syntaxes and concepts that are appropriate for both foundational developers and end-users. (9) Explore innovative metaphors and protocols for understanding, using, composing, searching, authenticating, and validating constructive results. (10) Examine models of applicable assurance structures and their economics. This research draws upon many disciplines including mathematics, logic, computer science, psychology, modeling and simulation, and software engineering economics.

Impact: Historically, libraries have greatly influenced society. Digital libraries of constructive algorithms and mathematics will certainly encourage excellence in program construction that will benefit the national infrastructures and, in particular, the information industries.

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.

February 2002