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.