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

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.