Paulo Oliva's research interests
In this page I will briefly describe my
main research interests, outlining some of the projects I'm currently
Logic (Functional Interpretations)
area of research is in mathematical logic and proof theory. In
particular, I am interested in the computational content of
mathematical proofs. What do theorems tell us, apart from the truth
they convey? How can proofs be viewed as programs, so as to be
executed, and how can programs be viewed as proofs, so that their
correctness can be automatically checked? These questions become highly
non-trivial when proofs involve classical logic, induction and
analytical principles such as countable choice and WKL.
The main technique used is the so-called functional interpretation,
whereby formal proofs are inductively associated with functionals of
higher type. Examples of functional interpretations include Gödel's Dialectica
interpretation and Kreisel's
I have recently developed a unifying framework for functional
interpretations, which allows for a comparison between several
functional interpretations (see ,  and
This framework has shown to be useful in combining the different
interpretations into a hybrid functional interpretation ,
making it possible to combine the features of each interpretation in
the analysis of each single proof.
Verification (Hoare Logic)
I have also been working on the application of formal verification to
the domain of
continuous systems. More precisely, developing 'Hoare logic' systems in
order to prove properties of systems in the continuous time domain .
research career was on the topic of algorithms. That was the time when
I was taking part in the ACM ICPC (International Collegiate Programming
Challenge). My first paper was is on pattern matching algorithms,
jointly written with K. Guimaraes and E. W. Myers .
Last updated on 3 June 2008 by Paulo Oliva