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

点击翻译按钮获取中文摘要

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.**