SHF: Small: A Higher-Order Framework for Meta-Theoretic Reasoning

University Of Minnesota-Twin Cities, Minneapolis MN

Investigators

Abstract

This project develops a logical framework that is well-adapted to the tasks of formulating and proving meta-theoretic properties of programming languages and the correctness of translators and compilers; these tasks arise naturally in the context of ensuring the safety and security of software. The framework being investigated is specialized to reasoning about relational specifications concerning formal objects that embody a binding structure. Such specifications simplify the encoding of formal systems that often treat syntactically complex constructs and that also manifest non-deterministic and non-terminating behavior. Underlying the framework is an expressive first-order logic that allows predicates to be interpreted through fixed-point definitions and that also includes inductive and co-inductive principles for reasoning about such definitions. One project goal is to enrich the form of definitions permitted in this logic and to add the ability to quantify over properties or predicates to it. Another goal is to develop a methodology for using the enhanced logic in actual verification tasks such as proving the correctness of compilers for functional languages. The project will make available to the research community an enhanced software system that supports formalization and verification tasks of the kind outlined. At a foundational level, the research leads to a better understanding of the interaction between inductive definitions and higher-order quantification, an issue that is important to many modern theorem-proving systems.