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

提出的研究的主要目标是推进技术的艺术状态证明程序和编程语言的性质。建议的工作属于形式化方法的领域，并关注于形式化证明，它有可能提供非常高水平的保证，以保持软件系统所需的属性（如安全性、隐私性、安全性和正确性）。这项工作的应用领域包括开发更安全的编程语言、更健壮的编译器和更值得信赖的软件。正式方法包括应用数学技术来显示软件达到了期望的高质量标准。形式证明包括使用软件系统来帮助证明定理。在这个领域中，定理表达了软件所需的属性。我们的方法是在建立在众所周知的逻辑基础上的现有交互式定理证明系统中为证明这些定理提供支持，并使用一种称为高阶抽象语法（HOAS）的技术来表示编程语言。我们过去的工作集中在一个叫做Hybrid的系统上。支持HOAS的系统为推理的各个方面提供了大量支持，例如变量、替换和假设上下文，具有极大简化此类推理中涉及的任务的潜力。*** *拟议工作的总体目标是显著地(a)改进现有技术，(b)开发使用HOAS进行推理的新技术，(c)提高该领域工具的可用性，以及(d)用坚实的理论支持这些工具功能和技术。我们的工作旨在改进混合方法，并突破边界，增加HOAS方法的功能和可用性。我们承担的项目主要分为四类。(1)我们将开展短期项目以提高Hybrid的可用性。(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.**