SHF:Small:Reasoning about Specifications of Computations

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.