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 Fundamentals of AI and Computational Theory2025
Uniform Functional InterpretationsOliva P
Lecture Notes in Computer Science. vol. 15764, 88-103.
01-01-2025
2022
Higher-order Games with Dependent TypesEscardó M Oliva P
In Arxiv
15-12-2022
2021
On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone TheoremArthan R Oliva P
Journal of Logic and Analysis, Journal of Logic and Analysis vol. 13
31-12-2021
On rational choice and the representation of decision problemsOliva P Zahn P
Games vol. 12 (4)
01-12-2021
A Parametrised Functional Interpretation of Heyting ArithmeticDinis B Oliva P
Annals of Pure and Applied Logic, 102940-102940.
07-01-2021
2020
On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone TheoremArthan R Oliva P
In Arxiv
17-12-2020
Double Negation Semantics for Generalisations of Heyting AlgebrasOliva P Arthan R
Studia Logica: An International Journal For Symbolic Logic, Springer Verlag
25-05-2020
Parametrised Functional InterpretationsDinis B Oliva P
In Arxiv
12-05-2020
Kripke Semantics for Intuitionistic Lukasiewicz LogicAndrew L-S Oliva P Robinson E
Studia Logica: An International Journal For Symbolic Logic, Springer Verlag
21-04-2020
2019
On the Herbrand Functional InterpretationOliva P Xu C
In Arxiv
03-12-2019
Negative Translations for Affine and Lukasiewicz LogicArthan R Oliva P
In Arxiv
29-11-2019
Studying Algebraic Structures Using Prover9 and Mace4Oliva P Arthan R
91-111.
02-10-2019
Studying Algebraic Structures using Prover9 and Mace4Arthan R Oliva P
In Arxiv
14-08-2019
An analysis of the Podelski-Rybalchenko termination theorem via bar recursionBerardi S Oliva P Steila S
Journal of Logic and Computation vol. 29 (4), 555-575.
01-08-2019
2018
A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz LogicArthan R Oliva P
In Arxiv
12-09-2018
A direct proof of Schwichtenberg's bar recursion closure theoremBORGES OLIVA P Steila S
The Journal of Symbolic Logic, Association For Symbolic Logic
12-02-2018
The Structure of the Environment and the Complexity of Rational Choice ProceduresZahn P Oliva P
In Ssrn Electronic Journal
01-01-2018
The Choice Environment, Constraints, and Rational ProceduresOliva P Zahn P
In Ssrn Electronic Journal
01-01-2018
2017
The Herbrand Functional Interpretation of the Double Negation ShiftBORGES OLIVA P Escardo M
The Journal of Symbolic Logic, Association For Symbolic Logic
19-06-2017
Higher-Order Decision TheoryHedges J Oliva P Shprits E Winschel V Zahn P
In Algorithmic Decision Theory, Springer Nature 241-254.
01-01-2017
2016
Selection Equilibria of Higher-Order GamesHedges J Oliva P Shprits E Winschel V Zahn P
PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES. vol. 10137, 136-151.
17-12-2016
Bar recursion over finite partial functionsOliva P Powell T
Annals of Pure and Applied Logic vol. 168 (5), 887-921.
09-11-2016
A Direct Proof of Schwichtenberg's Bar Recursion Closure TheoremOliva P Steila S
In Arxiv
18-07-2016
2015
A Game-Theoretic Computational Interpretation of Proofs in Classical AnalysisBORGES OLIVA P Powell T
In Gentzen's Centenary The Quest For Consistency, Springer
14-06-2015
Higher-Order Game TheoryHedges J Oliva P Sprits E Winschel V Zahn P
In Arxiv
02-06-2015
Higher-Order Decision TheoryHedges J Oliva P Sprits E Winschel V Zahn P
In Arxiv
02-06-2015
BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONSESCARDÓ M OLIVA P
Journal of Symbolic Logic, Cambridge University Press (Cup) vol. 80 (1), 1-28.
01-03-2015
2014
A constructive interpretation of Ramsey's theorem via the product of selection functionsOLIVA P POWELL T
Mathematical Structures in Computer Science, Cambridge University Press (Cup) vol. 25 (8), 1755-1778.
13-11-2014
The Herbrand Functional Interpretation of the Double Negation ShiftEscardo M Oliva P
In Arxiv
16-10-2014
A Higher-order Framework for Decision Problems and GamesHedges J Oliva P Winschel E Winschel V Zahn P
In Arxiv
25-09-2014
PrefaceOliva P
Electronic Proceedings in Theoretical Computer Science Eptcs. vol. 164
09-09-2014
Proceedings Fifth International Workshop on Classical Logic and ComputationOliva P
In Arxiv
09-09-2014
Bar Recursion and Products of Selection FunctionsEscardo M Oliva P
In Arxiv
25-07-2014
Proving termination with transition invariants of height omegaBerardi S Oliva P Steila S
In Arxiv
17-07-2014
On Affine Logic and Łukasiewicz LogicArthan R Oliva P
In Arxiv
02-04-2014
Proving termination of programs having transition invariants of height ωBerardi S Oliva P Steila S
Ceur Workshop Proceedings. vol. 1231, 237-240.
01-01-2014
2013
(Dual) Hoops Have Unique HalvingArthan R Oliva P
In Automated Reasoning and Mathematics, Springer Nature 165-180.
01-01-2013
2012
On the Relation Between Various Negative TranslationsFerreira G Oliva P
In Logic, Construction, Computation, De Gruyter 227-258.
31-12-2012
Hoops, Coops and the Algebraic Semantics of Continuous LogicArthan R Oliva P
In Arxiv
12-12-2012
Computing Nash Equilibria of Unbounded GamesEscardo M Oliva P
EPiC series in computing. vol. 10, 53-39.
22-06-2012
The Peirce translationEscardo M Oliva P
Annals of Pure and Applied Logic vol. 163 (6), 681-692.
01-01-2012
On bounded functional interpretationsFerreira G Oliva P
Annals of Pure and Applied Logic vol. 163 (8), 1030-1049.
01-01-2012
On Spector's bar recursionOliva P Powell T
Mathematical Logic Quarterly vol. 58 (4-5)
01-01-2012
2011
System T and the product of selection functionsEscardó M Oliva P Powell T
Leibniz International Proceedings in Informatics Lipics. vol. 12, 233-247.
01-12-2011
Sequential games and optimal strategiesEscardo M Oliva P
Proceedings of The Royal Society A vol. 467 (2130), 1519-1545.
08-06-2011
A Hoare logic for linear systemsOliva P Arthan R Martin U
Formal Aspects of Computing: Applicable Formal Methods, Springer London
01-05-2011
Functional interpretations of intuitionistic linear logicOliva P Ferreira G
Logical Methods in Computer Science, Institute of Theoretical Computer Science vol. 7 (1.9), 1-22.
01-03-2011
2010
Functional Interpretations of Intuitionistic Linear LogicFerreira G Oliva P
In Arxiv
06-12-2010
Proof interpretations with truthGaspar J Oliva P
Math Logic Quart vol. 56 (6), 591-610.
01-12-2010
What sequential games, the Tychnoff theorem and the double-negation shift have in commonEscardó M Oliva P
Mathematically Structured Functional Programming.
01-08-2010
Functional interpretations of linear and intuitionistic logicOliva P
INFORMATION AND COMPUTATION. vol. 208 (5), 565-577.
01-05-2010
Selection functions, bar recursion and backward inductionEscardo M Oliva P
Domains IX Brighton, UK 22 Sep 2008 - 24 Sep 2008. vol. 20 (2), 127-168.
01-04-2010
Functional Interpretations of Intuitionistic Linear LogicOliva P
Journal of Logic and Computation, Oxford Journals
09-02-2010
Hybrid functional interpretations of linear and intuitionistic logicOliva P
Journal of Logic and Computation, Oxford Journals vol. 22 (2), 305-328.
01-01-2010
Confined modified realizabilityFerreira G Oliva P
Mathematical Logic Quarterly vol. 56 (1), 13-28.
01-01-2010
Computational interpretations of analysis via products of selection functionsEscardó M Oliva P
Computability in Europe Azores. vol. 6158, 141-150.
01-01-2010
The Peirce translation and the double negation shiftEscardó M Oliva P
Computability in Europe Azores. (6158), 151-161.
01-01-2010
2009
Functional Interpretations of Intuitionistic Linear LogicFerreira G Oliva P
Computer Science Logic Coimbra, Portugal. vol. 5771, 3-19.
01-01-2009
2008
A General Framework for Sound and Complete Floyd-Hoare LogicsArthan R Martin U Mathiesen EA Oliva P
Acm Transactions on Computational Logic, 11(1), 2009
07-07-2008
Hybrid functional interpretationsHernest MD Oliva P Beckmann A Dimitracopoulos C Lowe B
LOGIC AND THEORY OF ALGORITHMS. vol. 5028, 251-260.
01-01-2008
On Krivine's realizability interpretation of classical second-order arithmeticOliva P Streicher T
FUNDAMENTA INFORMATICAE. vol. 84 (2), 207-220.
01-01-2008
An analysis of Godel's 'Dialectica' interpretation via linear logicOliva P
Dialectica vol. 62 (2), 269-290.
01-01-2008
2007
Bounded functional interpretation and feasible analysisFerreira F Oliva P
Ann Pure Appl Logic vol. 145 (2), 115-129.
01-02-2007
Modified realizability interpretation of classical linear logicOliva P
22nd Annual IEEE Symposium on Logic in Computer Science, Proceedings., 431-440.
01-01-2007
Computational interpretations of classical linear logicOliva P Leivant D DeQueiroz R
Logic, Language, Information and Computation, Proceedings. vol. 4576, 285-296.
01-01-2007
Reasoning about linear systemsArthan R Martin U Mathiesen EA Oliva P Hinchey M Margaria T
SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS., 123-132.
01-01-2007
2006
Unifying Functional InterpretationsOliva P
Notre Dame Journal of Formal Logic vol. 47 (2), 263-290.
01-07-2006
Modified bar recursionBerger U Oliva P
Math Struct Comp Sci vol. 16 (2), 163-183.
01-04-2006
Understanding and using Spector's bar recursive interpretation of classical analysisOliva P Beckmann A Berger U Lowe B Tucker JV
LOGICAL APPROACHES TO COMPUTATIONAL BARRIERS, PROCEEDINGS. vol. 3988, 423-434.
01-01-2006
Hoare logic in the abstractMartin U Mathiesen EA Oliva P Esik Z
COMPUTER SCIENCE LOGIC, PROCEEDINGS. vol. 4207, 501-515.
01-01-2006
2005
Bounded functional interpretationFerreira F Oliva P
Ann Pure Appl Logic vol. 135 (1-3), 73-112.
01-09-2005
Modified bar recursion and classical dependent choiceBerger U Oliva P Baaz M Friedman SD Krajicek J
Logic Colloquim 01, Proceedings. vol. 20, 89-107.
01-01-2005
2003
Proof mining in L-1-approximationKohlenbach U Oliva P
Ann Pure Appl Logic vol. 121 (1), 1-38.
15-05-2003
Polynomial-time algorithms from ineffective proofsOliva P
18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS., 128-137.
01-01-2003
Proof mining: A systematic way of analyzing proofs in mathematicsOliva P Kohlenbach U
Proc. Steklov Inst. Math vol. 242, 136-164.
01-01-2003
2002
On the computational complexity of best L-1-approximationOliva P
MATHEMATICAL LOGIC QUARTERLY. vol. 48, 66-77.
01-01-2002
1998
Reporting exact and approximate regular expression matchesMyers EW Oliva P Guimarães K
Lecture Notes in Computer Science. vol. 1448, 91-103.
01-01-1998
Uniform Functional InterpretationsOliva P
Computability in Europe Lisbon 14 Jul 2025 - 18 Jul 2025.
On the Herbrand Functional InterpretationOliva P Xu C
Mathematical Logic Quarterly, Wiley
Case Studies in Analogue Hardware VerificationMartin U GOTTLIEBSEN H Oliva P Mathiesen E
Conference on Computer Aided Verification, 2006.
Higher-order Games with Dependent TypesOliva P Escardo M
Theoretical Computer Science, Elsevier
Research Group
News
No news items found.