The research will develop the foundations for a framework for reasoning about the formal properties of programming languages, compilers, software specifications, concurrent systems and other related computational systems. The framework will be based on two separate but interacting logics. One logic will be geared towards specifying and prototyping varied software systems. The second logic, referred to as the meta-logic, will provide flexible and powerful mechanisms for reasoning about specifications written in the first logic. The objects to be specified and reasoned about typically have complex syntactic structures, often involving some form of binding. Use will be made of a higher-order approach to representing syntactic structure in both logics to facilitate a natural treatment of such objects. Useful new logical capabilities will be exposed and embedded in actual computer systems that can be used in prototyping and reasoning tasks in the intended domains. The insights and the tools produced will be used pedagogically to expose high-school students and beginning undergraduates to important ideas in logic and computation. A close collaboration with a group of French researchers will provide an international dimension to the research, co-funded in part by the NSF Office of International Science and Engineering. In the long run, mechanized formal specification of (and reasoning about) programming languages has clear application to the improvement of software infrastructure in the real world: its correctness, reliability, maintainability, and security.
Formal specifications have a significant role to play in the development of reliable hardware and software systems. Such specifications can be used in multiple ways in this context: they can provide the means for articulating the structure of these systems, they can later function as the yardsticks for their implementation, and they can eventually be used as the basis for establishing that the implementations have desirable properties. Given the overall importance of safe and secure computational systems to modern society, there is an obvious need to enable the effective use of formal specifications in these various forms. The objective of this project was to develop the foundations of a framework that can provide automated support for the use of formal specifications in the manner described above. There were two key desiderata for the framework. First, it needed to embody methodologies and tools for articulating and animating specifications so that they can be used in analyzing and prototyping the systems they describe. Second, the framework needed to support techniques for formally reasoning about specifications and, through this process, about the computational systems that implement them. While formal specifications can take a number of different forms, the focus in this project was on ones that are presented in a syntax-directed and rule-based manner; this style of specification is very flexible has therefore gained widespread use in practical settings. The central innovation in the project was that of constructing the described framework around two different but interacting logics. One of these logics, called the specification logic, is intended to provide a precise, formal basis for presenting rule-based specifications. By carefully calibrating this logic, we can provide it a computational interpretation; this would yield a means for executing specifications written in the logic and thereby for prototyping the systems they define. The second logic, called the reasoning logic, is intended to embed the specification logic and to reason about it using powerful techniques such as induction and case analysis: the ability to reason richly about specifications would then flow from the corresponding ability to reason about the logic in which they are encoded. The research conducted under the project has successfully elaborated on this vision. The work began with a specification logic that had been designed in past, NSF-funded work and that possessed several of the desired properties. The initial focus was on developing a reasoning logic that is both sound and sufficiently expressive. Once a candidate logic had been articulated, it was analyzed to ensure that it possessed the important theoretical properties. The next step was to develop a framework around this logic. This work culminated in the implementation of the framework in a system called Abella. Abella was experimented with in a variety of reasoning tasks aimed at understanding and demonstrating its effectiveness. One of the applications considered was that of compiler verification. The results have shown significant promise for the framework in this area. Project research also explored variants to the specification and reasoning logics. An especially intriguing possibility that has been considered is that of using a popular dependently typed lambda calculus specification language called LF within the framework. The project has provided varied opportunities for developing human and educational resources related to the science of building robust and reliable software. A postdoctoral fellow who has since joined the faculty of ENS Cachan, a top-ranked French university, and a doctoral student who is now a Senior Industrial Logician at Rockwell Collins were mentored under the grant. The project has provided the context for two ongoing doctoral theses and one completed Masters thesis. Five undergraduates have been involved in the work through supplemental funds provided by the NSF Research Experience for Undergraduates program. A graduate level course on specifying and reasoning about computational systems has been developed and offered at a European summer school, at the IT University of Copenhagen and at the University of Minnesota. This course has used the Abella system as well as a research monograph entitled "Programming with Higher-Order Logic" that is based on work partially supported by the grant. Finally, the grant has facilitated an interaction with a high school teacher aimed at developing course material and teaching techniques that can positively impact K-12 STEM-oriented education; this interaction was funded through the NSF Research Experience for Teachers program. The grant has fostered collaborations with related research groups in Australia, Canada and Europe. The most extensive of these collaborations has been with a group at INRIA, the French national institute for computer science research. Joint papers and computer systems have been produced as a result and students supported by the grant have had the opportunity to travel and work in France over an extended period.
