Skip to content
Go
Search RoyalSociety.org
Research Fellows Directory
#
Paulo Oliva

{
"@context": "http://schema.org",
"@type": "Person",
"name": "Paulo Oliva" ,
"honorificSuffix":"Royal Society Research Fellow",
"jobTitle":"Dr" ,
"honorificPrefix":"PhD" ,
"gender":"" ,
"worksFor": {
"@type": "Organization",
"name": "Queen Mary, University of London"
},
"image":""
}
#### Dr Paulo Oliva PhD

## Organisation

## Research summary

## Grants awarded

#### Selection functions in proof theory

#### Selection functions in proof theory

#### Functional interpretations and the nature of computing

#### Functional interpretations and the nature of computing

Back to top

You currently have JavaScript disabled in your web browser, please enable JavaScript to view our website as intended.

Here are the instructions of how to enable JavaScript in your browser.

Research Fellow

Queen Mary, University of London

My research area is in mathematical logic, or, more precisely, the logical structure of proofs in mathematics. I study proofs in Mathematics because proofs are very similar to computer programs (as in Computer Science). Just as complex computer systems are normally built in a modular fashion, out of smaller subcomponents; so are complex proofs in mathematics. When proving a new theorem, a mathematician is allowed to freely use other theorems already proven

by other mathematicians, just like software engineers are encouraged to reuse computer code, and build systems using standard libraries. From this perspective,

Mathematics can be thought of as a big open source project, very similar to the project that led to the development of the Linux operating system.

The problem is that Mathematics is a different form of programming language, which is not directly comprehensible to a standard computer. And moreover, it is

not an easy task to tell what a given proof in Mathematics will turn out to be once you convert it into a computer program. In order to be able to understand what a

proof does, and ultimately to “run” it just like to we with everyday computer software, we need a translator from the language of Mathematics to the language

of computers. I work both on such translation mechanisms but also on the particular meaning of the programs one obtains from some standard proof in

Mathematics.

The impact of my research lies on the potential to turn complex and clever proofs in Mathematics into sophisticated computer programs that we might not be able to come up with, or build, directly. We have some concrete examples of this. For instance, a 50-year old proof in approximation theory has been shown to solve an

algorithmic task no one had been able to solve otherwise. In this particular case, the proof had hidden in its logical structure a computational procedure to

approximate any continuous function by a polynomial.

**Scheme:** University Research Fellowship

**Dates:** Oct 2011 - Sep 2014

**Value:** £262,387.74

**Scheme:** University Research Fellowship

**Dates:** Oct 2006 - Sep 2011

**Value:** £394,464.80

Connect with us: Connect on Facebook Connect on Twitter Connect on YouTube Connect on LinkedIn Connect on Pinterest

Stay in touch: Email updates | Blogs | Podcasts and RSS feeds

Copyright © 2018 The Royal Society.

All rights reserved. Terms, conditions and policies.