Dr Paulo Oliva
My main 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.
Recently, 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.
My early 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.
Tutorial Speaker (MFPS) 2011-05-26 Tutorial speaker at the 2011 MFPS. Pittsburgh, 25-28 May, 2011.
Invited Speaker (Logic Collquium) 2010-07-25 Invited speaker at the 2010 Logic Colloquium. Paris, 25-31 July, 2010.
Invited speaker (TMCNAA'07) 2007-07-15 Invited speaker at the 1st Workshop on Traced Monoidal Categories, Network Algebras, and Applications. Wroclaw, 15 July, 2007.
Invited speaker (WoLLIC'07) 2007-07-02 Invited speaker at the 14th Workshop on Logic, Language, Information and Computation. Rio de Janeiro, 2-5 July, 2007.
Invited participant (Dagstuhl meeting) 2005-05-12 Talk given at the Dagstuhl meeting: Mathematics, Algorithms, Proofs Organised by T. Coquand (Chalmers - Göteborg, SE), H. Lombardi (Université de Franche-Comté, FR), M.-F. Roy (Université de Rennes, FR) http://www.dagstuhl.de/05021/
Invited speaker 2005-03-29 Workshop on applications of proof assistants. Organised by Professor Helmut Schwichtenberg. http://www.mathematik.uni-muenchen.de/~gkli/Venezia/
Invited participant (Oberwolfach meeting) 2005-03-20 Talk given at the Oberwolfach meeting on Mathematical Logic: Proof Theory, Type Theory and Constructive Mathematics. http://www.mfo.de/cgi-bin/tagungsdb?type=21&tnr=0512