EPSRC Reference: 
EP/W035847/1 
Title: 
Imperative programs from proofs 
Principal Investigator: 
Powell, Dr T R J 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Bath 
Scheme: 
New Investigator Award 
Starts: 
07 November 2022 
Ends: 
06 November 2025 
Value (£): 
311,440

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
28 Mar 2022

EPSRC ICT Prioritisation Panel March 2022

Announced


Summary on Grant Application Form 
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 correctbyconstruction 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 stateoftheart 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 realworld programming language. This will involve incorporating a global state along with control flow statements such as whileloops. 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 correctbyconstruction 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 crossdisciplinary, and we will exploit this by organising visits to a range of relevant research groups in the UK and internationally, and by hosting a crossdisciplinary workshop towards the end of the project.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.bath.ac.uk 