Dr Paulo Oliva
Reader in Mathematical Logic
Director of Outreach / Programme Director for Computer Science and Mathematics
School of Electronic Engineering and Computer Science
Queen Mary University of London
Queen Mary University of London
Research
mathematical logic, proof theory, formal verification, algorithms
Interests
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 on pattern matching algorithms, jointly written with K. Guimaraes and E. W. Myers.
Publications
Publications of specific relevance to the Centre for Fundamental Computer Science2023
Escardó M and Oliva P (2023). Higher-order games with dependent types. Theoretical Computer Science, Elsevier vol. 974 01-09-2023
2021
Arthan R and Oliva P (2021). On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem. Journal of Logic and Analysis, Journal of Logic and Analysis vol. 13 31-12-2021
Oliva P and Zahn P (2021). On rational choice and the representation of decision problems. Games vol. 12 (4) 01-12-2021
Dinis B and Oliva P (2021). A Parametrised Functional Interpretation of Heyting Arithmetic. Annals of Pure and Applied Logic, 102940-102940. 07-01-2021
2020
Oliva P and Arthan R (2020). Double Negation Semantics for Generalisations of Heyting Algebras. Studia Logica: an international journal for symbolic logic, Springer Verlag 25-05-2020
Andrew L-S, Oliva P and Robinson E (2020). Kripke Semantics for Intuitionistic Lukasiewicz Logic. Studia Logica: an international journal for symbolic logic, Springer Verlag 21-04-2020
Oliva P and Xu C (2020). On the Herbrand functional interpretation. Mathematical Logic Quarterly, Wiley vol. 66 (1), 91-98. 01-03-2020
2019
Oliva P and Arthan R (2019). Studying Algebraic Structures Using Prover9 and Mace4. 91-111. 02-10-2019
Berardi S, Oliva P and Steila S (2019). An analysis of the Podelski-Rybalchenko termination theorem via bar recursion. JOURNAL OF LOGIC AND COMPUTATION vol. 29 (4), 555-575. 01-08-2019
2018
BORGES OLIVA P and Steila S (2018). A direct proof of Schwichtenberg's bar recursion closure theorem. The Journal of Symbolic Logic, Association for Symbolic Logic 12-02-2018
2017
BORGES OLIVA P and Escardo M (2017). The Herbrand Functional Interpretation of the Double Negation Shift. The Journal of Symbolic Logic, Association for Symbolic Logic 19-06-2017
Hedges J, Oliva P, Shprits E, Winschel V and Zahn P (2017). Higher-Order Decision Theory. Algorithmic Decision Theory 241-254. 01-01-2017
2016
Hedges J, Oliva P, Shprits E, Winschel V and Zahn P (2016). Selection Equilibria of Higher-Order Games. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES. 17-12-2016
Oliva P and Powell T (2016). Bar recursion over finite partial functions. ANNALS OF PURE AND APPLIED LOGIC vol. 168 (5), 887-921. 09-11-2016
2015
BORGES OLIVA P and Powell T (2015). A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis. Gentzen's Centenary The Quest for Consistency , Editors: Kahle R and Rathjen M. 14-06-2015
ESCARDÓ M and OLIVA P (2015). BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS. Journal of Symbolic Logic, Cambridge University Press (CUP) vol. 80 (1), 1-28. 01-03-2015
2014
OLIVA P and POWELL T (2014). A constructive interpretation of Ramsey's theorem via the product of selection functions. Mathematical Structures in Computer Science, Cambridge University Press (CUP) vol. 25 (8), 1755-1778. 13-11-2014
Oliva P (2014). Proceedings Fifth International Workshop on Classical Logic and Computation. Electronic Proceedings in Theoretical Computer Science, Open Publishing Association vol. 164 09-09-2014
Berardi S, Oliva P and Steila S (2014). Proving termination of programs having transition invariants of height ω. 01-01-2014
2013
Arthan R and Oliva P (2013). (Dual) Hoops Have Unique Halving. Automated Reasoning and Mathematics 165-180. 01-01-2013
2012
Ferreira G and Oliva P (2012). On the Relation Between Various Negative Translations. Logic, Construction, Computation 227-258. 31-12-2012
Escardo M and Oliva P (2012). The Peirce translation. ANNALS OF PURE AND APPLIED LOGIC vol. 163 (6), 681-692. 01-01-2012
Ferreira G and Oliva P (2012). On bounded functional interpretations. ANNALS OF PURE AND APPLIED LOGIC vol. 163 (8), 1030-1049. 01-01-2012
Oliva P and Powell T (2012). On Spector's bar recursion. MATHEMATICAL LOGIC QUARTERLY vol. 58 (4-5) 01-01-2012
2011
Escardo M and Oliva P (2011). Sequential games and optimal strategies. Proceedings of the Royal Society A vol. 467 (2130), 1519-1545. 08-06-2011
Oliva P, Arthan R and Martin U (2011). A Hoare logic for linear systems. Formal Aspects of Computing: applicable formal methods, Springer London 01-05-2011
Oliva P and Ferreira G (2011). Functional interpretations of intuitionistic linear logic. Logical Methods in Computer Science, Institute of Theoretical Computer Science vol. 7 (1.9), 1-22. 01-03-2011
2010
Gaspar J and Oliva P (2010). Proof interpretations with truth. MATH LOGIC QUART vol. 56 (6), 591-610. 01-12-2010
Escardó M and Oliva P (2010). What sequential games, the Tychnoff theorem and the double-negation shift have in common. Mathematically Structured Functional Programming. 01-08-2010
Escardo M and Oliva P (2010). Selection functions, bar recursion and backward induction. Domains IX Brighton, UK 22 Sep 2008 - 24 Sep 2008. 01-04-2010
Oliva P (2010). Functional Interpretations of Intuitionistic Linear Logic. Journal of Logic and Computation, Oxford Journals 09-02-2010
Oliva P (2010). Hybrid functional interpretations of linear and intuitionistic logic. Journal of Logic and Computation, Oxford Journals vol. 22 (2), 305-328. 01-01-2010
Ferreira G and Oliva P (2010). Confined modified realizability. Mathematical Logic Quarterly vol. 56 (1), 13-28. 01-01-2010
Escardó M and Oliva P (2010). Computational interpretations of analysis via products of selection functions. Computability in Europe Azores. 01-01-2010
Escardó M and Oliva P (2010). The Peirce translation and the double negation shift. Computability in Europe Azores. 01-01-2010
2009
Ferreira G and Oliva P (2009). Functional Interpretations of Intuitionistic Linear Logic. Computer Science Logic Coimbra, Portugal. 01-01-2009
2008
Arthan R, Martin U, Mathiesen EA and Oliva P (2008). A General Framework for Sound and Complete Floyd-Hoare Logics. ACM Transactions on Computational Logic, 11(1), 2009 07-07-2008
Hernest MD and Oliva P (2008). Hybrid functional interpretations., Editors: Beckmann A, Dimitracopoulos C and Lowe B. 01-01-2008
Oliva P and Streicher T (2008). On Krivine's realizability interpretation of classical second-order arithmetic. 01-01-2008
Oliva P (2008). An analysis of Godel's 'Dialectica' interpretation via linear logic. DIALECTICA vol. 62 (2), 269-290. 01-01-2008
2007
Ferreira F and Oliva P (2007). Bounded functional interpretation and feasible analysis. ANN PURE APPL LOGIC vol. 145 (2), 115-129. 01-02-2007
Oliva P (2007). Computational interpretations of classical linear logic., Editors: Leivant D and DeQueiroz R. 01-01-2007
Arthan R, Martin U, Mathiesen EA and Oliva P (2007). Reasoning about linear systems., Editors: Hinchey M and Margaria T. 01-01-2007
2006
Oliva P (2006). Unifying Functional Interpretations. Notre Dame Journal of Formal Logic vol. 47 (2), 263-290. 01-07-2006
Berger U and Oliva P (2006). Modified bar recursion. MATH STRUCT COMP SCI vol. 16 (2), 163-183. 01-04-2006
Oliva P (2006). Understanding and using Spector's bar recursive interpretation of classical analysis., Editors: Beckmann A, Berger U, Lowe B and Tucker JV. 01-01-2006
Martin U, Mathiesen EA and Oliva P (2006). Hoare logic in the abstract., Editors: Esik Z. 01-01-2006
2005
Ferreira F and Oliva P (2005). Bounded functional interpretation. ANN PURE APPL LOGIC vol. 135 (1-3), 73-112. 01-09-2005
Berger U and Oliva P (2005). Modified bar recursion and classical dependent choice., Editors: Baaz M, Friedman SD and Krajicek J. 01-01-2005
2003
Kohlenbach U and Oliva P (2003). Proof mining in L-1-approximation. ANN PURE APPL LOGIC vol. 121 (1), 1-38. 15-05-2003
Oliva P and Kohlenbach U (2003). Proof mining: A systematic way of analyzing proofs in mathematics. Proc. Steklov Inst. Math vol. 242, 136-164. 01-01-2003
2002
1998
Myers EW, Oliva P and Guimarães K (1998). Reporting exact and approximate regular expression matches. 01-01-1998