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

点击翻译按钮获取中文摘要

This project develops a logical framework that is well-adaptedto the tasks of formulating and proving meta-theoretic properties ofprogramming languages and the correctness of translators andcompilers; these tasks arise naturally in the context of ensuring thesafety 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 allowspredicates to be interpreted through fixed-point definitions and thatalso includes inductive and co-inductive principles for reasoningabout such definitions. One project goal is to enrich the form ofdefinitions permitted in this logic and to add the ability to quantifyover 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 afoundational level, the research leads to a better understandingof the interaction between inductive definitions and higher-orderquantification, an issue that is important to many moderntheorem-proving systems.