| EPSRC Reference: |
EP/H011803/1 |
| Title: |
Computation-Sensitive Proofs |
| Principal Investigator: |
Oliva, Dr P |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Queen Mary University of London |
| Scheme: |
First Grant - Revised 2009 |
| Starts: |
01 January 2010 |
Ends: |
30 June 2011 |
Value (£): |
101,310
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Logic & Combinatorics |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
14 Jul 2009
|
ICT Prioritisation Panel (July 09)
|
Announced
|
|
|
Summary on Grant Application Form |
|
Proof mining stands for the process of logically analysing formal proofs with the aim of obtaining new (hidden) information from such proofs. For instance, a proof that certain iteration of a function converges to one of its fixed point might have hidden information about the rate at which the sequence converges (rate of convergence), or, a proof that a continuous function has a unique best approximation will normally contain a (potentially implicit) algorithm for constructing the polynomial out of any given function (modulus of uniqueness). The extraction of computational information from ineffective proofs often require a systematic analysis guided by methods of proof theory, such as proof translations and functional interpretations (e.g. realizability). These techniques have recently been shown to yield new interesting mathematical theorems out of old proofs, particularly in functional analysis (approximation theory and fixed point theory). The proposed project aims to develop new proof mining techniques and carry out concrete case studies in both computer science and mathematics, with the emphasis on the role of the structural rule of contraction in the complexity of the extracted programs. We will focus on the recent technique of hybrid functional interpretation which allows optimal use of several functionals interpretations when analysing a single proof. The technique will be implemented in a proof assistant, and case studies will be carried out.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic 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: |
|