Dr Paulo Oliva

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
ResearcherID ORCID Google Scholar LinkedIn

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

solid heart iconPublications of specific relevance to the Centre for Fundamental Computer Science

2023

Relevant PublicationHigher-order games with dependent types
Escardó M and Oliva P
Theoretical Computer Science, Elsevier vol. 974 
01-09-2023

2021

bullet iconOn the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem
Arthan R and Oliva P
Journal of Logic and Analysis, Journal of Logic and Analysis vol. 13 
31-12-2021
bullet iconOn rational choice and the representation of decision problems
Oliva P and Zahn P
Games vol. 12 (4) 
01-12-2021
bullet iconA Parametrised Functional Interpretation of Heyting Arithmetic
Dinis B and Oliva P
Annals of Pure and Applied Logic, 102940-102940.  
07-01-2021

2020

bullet iconDouble Negation Semantics for Generalisations of Heyting Algebras
Oliva P and Arthan R
Studia Logica: An International Journal For Symbolic Logic, Springer Verlag 
25-05-2020
Relevant PublicationKripke Semantics for Intuitionistic Lukasiewicz Logic
Andrew L-S, Oliva P and Robinson E
Studia Logica: An International Journal For Symbolic Logic, Springer Verlag 
21-04-2020
bullet iconOn the Herbrand functional interpretation
Oliva P and Xu C
Mathematical Logic Quarterly, Wiley vol. 66 (1), 91-98.  
01-03-2020

2019

bullet iconStudying Algebraic Structures Using Prover9 and Mace4
Oliva P and Arthan R
91-111.  
02-10-2019
bullet iconAn analysis of the Podelski-Rybalchenko termination theorem via bar recursion
Berardi S, Oliva P and Steila S
Journal of Logic and Computation vol. 29 (4), 555-575.  
01-08-2019

2018

bullet iconA direct proof of Schwichtenberg's bar recursion closure theorem
BORGES OLIVA P and Steila S
The Journal of Symbolic Logic, Association For Symbolic Logic 
12-02-2018

2017

bullet iconThe Herbrand Functional Interpretation of the Double Negation Shift
BORGES OLIVA P and Escardo M
The Journal of Symbolic Logic, Association For Symbolic Logic 
19-06-2017
bullet iconHigher-Order Decision Theory
Hedges J, Oliva P, Shprits E, Winschel V and Zahn P
In Algorithmic Decision Theory, Springer Nature 241-254.  
01-01-2017

2016

bullet iconSelection Equilibria of Higher-Order Games
Hedges J, Oliva P, Shprits E, Winschel V and Zahn P
PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES
17-12-2016
bullet iconBar recursion over finite partial functions
Oliva P and Powell T
Annals of Pure and Applied Logic vol. 168 (5), 887-921.  
09-11-2016

2015

bullet iconA Game-Theoretic Computational Interpretation of Proofs in Classical Analysis
BORGES OLIVA P and Powell T
In Gentzen's Centenary The Quest For Consistency, Springer, Editors: Kahle R and Rathjen M. 
14-06-2015
bullet iconBAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS
ESCARDÓ M and OLIVA P
Journal of Symbolic Logic, Cambridge University Press (Cup) vol. 80 (1), 1-28.  
01-03-2015

2014

bullet iconA constructive interpretation of Ramsey's theorem via the product of selection functions
OLIVA P and POWELL T
Mathematical Structures in Computer Science, Cambridge University Press (Cup) vol. 25 (8), 1755-1778.  
13-11-2014
bullet iconProceedings Fifth International Workshop on Classical Logic and Computation
Oliva P
Electronic Proceedings in Theoretical Computer Science, Open Publishing Association vol. 164 
09-09-2014
bullet iconPreface
Oliva P
 
09-09-2014
bullet iconProving termination of programs having transition invariants of height ω
Berardi S, Oliva P and Steila S
 
01-01-2014

2013

bullet icon(Dual) Hoops Have Unique Halving
Arthan R and Oliva P
In Automated Reasoning and Mathematics, Springer Nature 165-180.  
01-01-2013

2012

bullet iconOn the Relation Between Various Negative Translations
Ferreira G and Oliva P
In Logic, Construction, Computation, De Gruyter 227-258.  
31-12-2012
bullet iconThe Peirce translation
Escardo M and Oliva P
Annals of Pure and Applied Logic vol. 163 (6), 681-692.  
01-01-2012
bullet iconOn bounded functional interpretations
Ferreira G and Oliva P
Annals of Pure and Applied Logic vol. 163 (8), 1030-1049.  
01-01-2012
bullet iconOn Spector's bar recursion
Oliva P and Powell T
Mathematical Logic Quarterly vol. 58 (4-5) 
01-01-2012

2011

bullet iconSystem T and the product of selection functions
Escardó M, Oliva P and Powell T
 
01-12-2011
bullet iconSequential games and optimal strategies
Escardo M and Oliva P
Proceedings of The Royal Society A vol. 467 (2130), 1519-1545.  
08-06-2011
bullet iconA Hoare logic for linear systems
Oliva P, Arthan R and Martin U
Formal Aspects of Computing: Applicable Formal Methods, Springer London 
01-05-2011
bullet iconFunctional interpretations of intuitionistic linear logic
Oliva P and Ferreira G
Logical Methods in Computer Science, Institute of Theoretical Computer Science vol. 7 (1.9), 1-22.  
01-03-2011
bullet iconOn Various Negative Translations
Ferreira G and Oliva P
 
27-01-2011

2010

bullet iconProof interpretations with truth
Gaspar J and Oliva P
Math Logic Quart vol. 56 (6), 591-610.  
01-12-2010
bullet iconWhat sequential games, the Tychnoff theorem and the double-negation shift have in common
Escardó M and Oliva P
Mathematically Structured Functional Programming
01-08-2010
bullet iconFunctional interpretations of linear and intuitionistic logic
Oliva P
 
01-05-2010
bullet iconSelection functions, bar recursion and backward induction
Escardo M and Oliva P
Domains IX Brighton, UK 22 Sep 2008 - 24 Sep 2008
01-04-2010
bullet iconFunctional Interpretations of Intuitionistic Linear Logic
Oliva P
Journal of Logic and Computation, Oxford Journals 
09-02-2010
bullet iconHybrid functional interpretations of linear and intuitionistic logic
Oliva P
Journal of Logic and Computation, Oxford Journals vol. 22 (2), 305-328.  
01-01-2010
bullet iconConfined modified realizability
Ferreira G and Oliva P
Mathematical Logic Quarterly vol. 56 (1), 13-28.  
01-01-2010
bullet iconComputational interpretations of analysis via products of selection functions
Escardó M and Oliva P
Computability in Europe Azores
01-01-2010
bullet iconThe Peirce translation and the double negation shift
Escardó M and Oliva P
Computability in Europe Azores
01-01-2010

2009

bullet iconFunctional Interpretations of Intuitionistic Linear Logic
Ferreira G and Oliva P
Computer Science Logic Coimbra, Portugal
01-01-2009

2008

bullet iconA General Framework for Sound and Complete Floyd-Hoare Logics
Arthan R, Martin U, Mathiesen EA and Oliva P
Acm Transactions On Computational Logic, 11(1), 2009 
07-07-2008
bullet iconHybrid functional interpretations
Hernest MD and Oliva P
, Editors: Beckmann A, Dimitracopoulos C and Lowe B. 
01-01-2008
bullet iconOn Krivine's realizability interpretation of classical second-order arithmetic
Oliva P and Streicher T
 
01-01-2008
bullet iconAn analysis of Godel's 'Dialectica' interpretation via linear logic
Oliva P
Dialectica vol. 62 (2), 269-290.  
01-01-2008

2007

bullet iconBounded functional interpretation and feasible analysis
Ferreira F and Oliva P
Ann Pure Appl Logic vol. 145 (2), 115-129.  
01-02-2007
bullet iconModified realizability interpretation of classical linear logic
Oliva P
 
01-01-2007
bullet iconComputational interpretations of classical linear logic
Oliva P
, Editors: Leivant D and DeQueiroz R. 
01-01-2007
bullet iconReasoning about linear systems
Arthan R, Martin U, Mathiesen EA and Oliva P
, Editors: Hinchey M and Margaria T. 
01-01-2007

2006

bullet iconUnifying Functional Interpretations
Oliva P
Notre Dame Journal of Formal Logic vol. 47 (2), 263-290.  
01-07-2006
bullet iconModified bar recursion
Berger U and Oliva P
Math Struct Comp Sci vol. 16 (2), 163-183.  
01-04-2006
bullet iconUnderstanding and using Spector's bar recursive interpretation of classical analysis
Oliva P
, Editors: Beckmann A, Berger U, Lowe B and Tucker JV. 
01-01-2006
bullet iconHoare logic in the abstract
Martin U, Mathiesen EA and Oliva P
, Editors: Esik Z. 
01-01-2006
bullet iconUnifying Functional Interpretations
Oliva P
 
01-01-2006

2005

bullet iconBounded functional interpretation
Ferreira F and Oliva P
Ann Pure Appl Logic vol. 135 (1-3), 73-112.  
01-09-2005
bullet iconModified bar recursion and classical dependent choice
Berger U and Oliva P
, Editors: Baaz M, Friedman SD and Krajicek J. 
01-01-2005

2003

bullet iconProof mining in L-1-approximation
Kohlenbach U and Oliva P
Ann Pure Appl Logic vol. 121 (1), 1-38.  
15-05-2003
bullet iconPolynomial-time algorithms from ineffective proofs
Oliva P
 
01-01-2003
bullet iconProof mining: A systematic way of analyzing proofs in mathematics
Oliva P and Kohlenbach U
Proc. Steklov Inst. Math vol. 242, 136-164.  
01-01-2003

2002

bullet iconOn the computational complexity of best L-1-approximation
Oliva P
 
01-01-2002

1998

bullet iconReporting exact and approximate regular expression matches
Myers EW, Oliva P and Guimarães K
 
01-01-1998