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.