Imperative programs from proofs

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

The aim of this project is to develop new logical methods for extracting programs from mathematical proofs. Traditionally, such programs are extremely complicated and difficult to understand. We will improve the situation by devising novel techniques that produce programs written in a more natural language, thereby making program extraction more effective in several areas in which it is currently being applied.Background: It has long been known that there is a deep connection between logic and computation, and that mathematical proofs can be converted to computer programs. Proof interpretations are a technique for doing this. They are useful for many reasons. When implemented in a computer, they provide us with a way of synthesising programs that are correct-by-construction and therefore guaranteed to be bug free. When applied to complex mathematical proofs, they can sometimes reveal new algorithms that have not been previously discovered. There is now a large subfield of logic dedicated to using proof interpretation to extract programs from proofs.The problem: Proof interpretations are formal mathematical techniques, and as such they often result in programs that are quite different from those a human would write. These programs tend to be written in a very abstract language and can be extremely long, syntactic, and difficult to understand. This represents a drawback to using proof interpretations for practical purposes: While it is useful to have a program that we know accomplishes a particular task, it would be more useful if we were able to understand how that program worked!My main goal:This project aims to bring programs obtained using proof interpretations closer to those a human would write. The aim is to improve the current state-of-the-art so that extracted programs are written in a more natural language and therefore easier to understand.My approach: We will take one of the most powerful and widely used of all proof interpretations - K. Goedel's Dialectica interpretation - and adapt it so that it produces programs in a language that is much closer in spirit to a real-world programming language. This will involve incorporating a global state along with control flow statements such as while-loops. These are all core features of everyday languages such as C and Python but are absent from the kind of theoretical languages traditionally associated with proof interpretations. We will then further refine the new interpretation so that it is optimized for the two main applications outlined above: (i) synthesising correct-by-construction programs, and (ii) revealing interesting new algorithms from complex mathematical proofs. These two applications will each require a different approach, and the second in particular will involve a number of deep ideas from mathematical logic. We will then demonstrate our new technique by carrying out a series of case studies, targeting problem areas (i) and (ii) respectively and aimed at specific communities who would most benefit from our new method. In parallel, we will explore generalisations of our new method so that it could potentially incorporate further interesting structures from programming.The project will require us to bring together ideas from both mathematical logic and the theory of programming languages, and the intended applications, which will be exemplified through our case studies, bring formal verification and pure mathematics into play. This makes the project fundamentally cross-disciplinary, and we will exploit this by organising visits to a range of relevant research groups in the UK and internationally, and by hosting a cross-disciplinary workshop towards the end of the project.