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

所提议的研究的主要目标是推进证明程序和编程语言的性质的技术的最新水平。建议的工作属于正式方法的领域，并侧重于正式证明，它有可能提供软件系统所需属性(如安全性、保密性、安全性和正确性)所具有的极高级别的保证。这项工作的应用领域包括开发更安全的编程语言、更健壮的编译器和更值得信赖的软件。通常，正式方法涉及应用数学技术来证明软件达到了所需的高标准质量。形式证明涉及到使用辅助证明定理的软件系统。在这个领域中，定理表达了软件所需的属性。我们的方法是在现有的建立在众所周知的逻辑基础上的交互式定理证明系统中为证明这样的定理提供支持，并使用一种被称为高阶抽象语法(HOAS)的技术来表示编程语言。我们过去的工作集中在一个称为混合的系统上。支持HOA的系统为推理的各个方面提供了实质性的支持，如变量、替换和假设的上下文，有可能极大地简化此类推理所涉及的任务。我们表示，拟议工作的总体目标是显著地(A)改进现有技术和(B)开发使用HOA进行推理的新技术，(C)提高该领域工具的可用性，以及(D)以坚实的理论支持这些工具特征和技术。我们的工作旨在既改进混合方法，又推动居者有其屋方法的边界，并总体上增加居者有其屋方法的能力和可用性。(1)我们将进行短期项目，以提高混合软件的可用性。(2)我们会继续过去的工作，比较多个支援居屋津贴的制度，以便更深入了解现行的优点和缺点。(3)我们将为允许人们在系统之间进行翻译并在它们之间共享证明的理论基础做出贡献。(4)我们会进行一项大型个案研究，可能会综合运用不同的系统，以说明居者有其屋计划的优点，并为日后的研究工作指明方向。

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.