Grant: Discovery Grants Program - Individual

The principle objective of the proposed research is to advance the state of the art in techniques for proving properties of programming languages, logics, and other formal systems. 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 the desired properties hold. Our focus will be on application areas that benefit from the use of features of linear logic embedded into proof assistants, such as establishing properties of quantum programming languages, reasoning about biological networks, and formalizing proof theoretic results such as cut-elimination for a wide variety of linear logics. 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 or system. Our approach uses logical frameworks, which are general languages/logics with supporting tools in which it is possible to represent a wide variety of formal systems. Such frameworks are designed to capture uniformities of the systems being reasoned about and to provide support for such reasoning. In recent developments, logical frameworks implementing linear logic have been considered. They capture uniformities of formal systems with linear properties, such as the application areas mentioned above that are the focus of this work. The overall objectives of the proposed work are to (a) improve existing techniques and (b) develop new ones for reasoning about languages with linear features, to (c) improve the usability of tools in this domain, and to (d) back up these tool features and techniques with solid theory. A long term overarching goal is to build a logical framework that can be used by the research community at large, particularly those developing new programming languages, new biological models, and new logics, providing them with the ability to prove (and modify) the properties they are interested in as their languages, models, or logics evolve over time. The projects we undertake will fall into four main categories. (1) We will design, implement, and develop the theory of a linear logical framework that captures the commonalities of formal systems in a variety of application areas such as those mentioned above. (2) We will provide support for automating reasoning in this logical framework, including a library of definitions and lemmas and procedures for automating their proofs. (3) We will examine a complementary approach that involves capturing linear features as predicates, and develop the theory required to do so in a principled way. (4) We will carry out both proof-of-concept as well as larger case studies that compare the approaches, push the boundaries of current capabilities, and point the way forward for future research efforts.