A Higher-Order Abstract Syntax Approach to Reasoning about Programs and Programming Languages

建议的研究的主要目标是推进最先进的技术证明程序和编程语言的属性。 拟议的工作福尔斯正式方法的领域，并侧重于正式证明，这有可能提供一个非常高的保证水平，所需的属性的软件系统（如安全，隐私，安全性和正确性）举行。 这项工作的应用领域包括开发更安全的编程语言，更强大的编译器和更值得信赖的软件。 形式化方法涉及应用数学技术来证明软件达到了所期望的高质量标准。形式证明涉及使用软件系统来帮助证明定理。 在这个领域中，定理表达了软件的期望属性。 我们的方法是提供支持，以证明这些定理在现有的交互式定理证明系统建立在众所周知的逻辑基础，并使用一种技术，用于表示编程语言被称为高阶抽象语法（HOAS）。 我们过去的工作集中在一个称为混合的系统上。 支持HOAS的系统为推理的各个方面提供了实质性的支持，例如变量，替换和假设的上下文，有可能大大简化这种推理中涉及的任务。 建议的工作的总体目标是显着（a）改善现有的技术和（B）开发新的推理使用HOAS，（c）提高工具的可用性在这一领域，（d）备份这些工具的功能和技术与坚实的理论。 我们的工作旨在改进混合方法，并推动边界，提高HOAS方法的功能和可用性。 我们承接的项目将分为四大类。 (1)我们将参与短期项目，以提高混合的可用性。 (2)我们将继续我们过去的工作，比较各种支持HOAS的系统，有助于更好地了解当前的优势和劣势。 (3)我们将有助于理论基础，使人们能够在系统之间进行翻译，并在它们之间共享证明。 (4)我们将进行一个大的案例研究，可能使用不同的系统的组合，说明HOAS方法的优势，并指出未来的研究工作的方向。

The principle objective of the proposed research is to advance the state of the art in techniques for proving properties of programs and programming languages. The proposed work falls within the area of formal methods and focuses on formal proof, which has the potential to provide an exceptionally high level of assurance that desired properties of software systems (such as safety, privacy, security, and correctness) hold. Application areas for this work include developing more secure programming languages, more robust compilers, and more trustworthy software in general.     Formal methods involve applying mathematical techniques to show that software achieves this desired high standard of quality. Formal proof involves using software systems that assist in proving theorems. In this domain, theorems express the desired properties of the software. Our approach is to provide support for proving such theorems within existing interactive theorem proving systems built on well-known logical foundations, and to use a technique for representing programming languages known as higher-order abstract syntax (HOAS). Our past work has focused on a system called Hybrid.  Systems supporting HOAS provide substantial support for various aspects of reasoning, such as variables, substitutions, and contexts of assumptions, with the potential to greatly simplify the tasks involved in such reasoning.     The overall objectives of the proposed work are to significantly (a) improve existing techniques and (b) develop new ones for reasoning using HOAS, to (c) improve the usability of tools in this domain, and to (d) back up these tool features and techniques with solid theory. Our work aims to both improve the Hybrid approach in particular, and push the boundaries and increase the capabilities and usability of the HOAS approach in general.     The projects we undertake will fall into four main categories. (1) We will engage in shorter term projects to improve the usability of Hybrid. (2) We will continue our past work in comparing a variety of systems that support HOAS, contributing to a better understanding of current strengths and weaknesses. (3) We will contribute to the theoretical foundations that allow one to translate between systems and share proofs between them. (4) We will undertake a large case study, possibly using a combination of different systems, that illustrates the advantages of the HOAS approach, and points the way forward for future research efforts.