Skip to main content
Research
  1. Queen Mary University of London
  2. Research
  3. Publications

Publications: DR Paulo Oliva

Back to Search
Oliva P ( 2025 ) . Uniform Functional Interpretations . Lecture Notes in Computer Science . vol. 15764 , 88 - 103 .
Escardó M, Oliva P ( 2022 ) . Higher-order Games with Dependent Types .
Arthan R, Oliva P ( 2021 ) . On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem . Journal of Logic and Analysis vol. 13 ,
Oliva P, Zahn P ( 2021 ) . On rational choice and the representation of decision problems . Games vol. 12 , ( 4 )
Dinis B, Oliva P ( 2021 ) . A Parametrised Functional Interpretation of Heyting Arithmetic . Annals of Pure and Applied Logic102940 - 102940 .
Arthan R, Oliva P ( 2020 ) . On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem .
Oliva P, Arthan R ( 2020 ) . Double Negation Semantics for Generalisations of Heyting Algebras . Studia Logica: an international journal for symbolic logic
Dinis B, Oliva P ( 2020 ) . Parametrised Functional Interpretations .
Andrew L-S, Oliva P, Robinson E ( 2020 ) . Kripke Semantics for Intuitionistic Lukasiewicz Logic . Studia Logica: an international journal for symbolic logic
Oliva P, Xu C ( 2019 ) . On the Herbrand Functional Interpretation .
Arthan R, Oliva P ( 2019 ) . Negative Translations for Affine and Lukasiewicz Logic .
Oliva P, Arthan R ( 2019 ) . Studying Algebraic Structures Using Prover9 and Mace4 . Springer
Arthan R, Oliva P ( 2019 ) . Studying Algebraic Structures using Prover9 and Mace4 .
Berardi S, Oliva P, Steila S ( 2019 ) . An analysis of the Podelski-Rybalchenko termination theorem via bar recursion . JOURNAL OF LOGIC AND COMPUTATION vol. 29 , ( 4 ) 555 - 575 .
Arthan R, Oliva P ( 2018 ) . A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic .
BORGES OLIVA P, Steila S ( 2018 ) . A direct proof of Schwichtenberg's bar recursion closure theorem . The Journal of Symbolic Logic
Oliva P, Zahn P ( 2018 ) . The Choice Environment, Constraints, and Rational Procedures .
Zahn P, Oliva P ( 2018 ) . The Structure of the Environment and the Complexity of Rational Choice Procedures .
Hedges J, Oliva P, Shprits E, Winschel V, Zahn P ( 2017 ) . Higher-Order Decision Theory . Algorithmic Decision Theory , vol. 10576 , Springer Nature
BORGES OLIVA P, Escardo M ( 2017 ) . The Herbrand Functional Interpretation of the Double Negation Shift . The Journal of Symbolic Logic
Hedges J, Oliva P, Shprits E, Winschel V, Zahn P ( 2016 ) . Selection Equilibria of Higher-Order Games . PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES (PADL 2017) . Conference: PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES vol. 10137 , 136 - 151 .
Oliva P, Powell T ( 2016 ) . Bar recursion over finite partial functions . ANNALS OF PURE AND APPLIED LOGIC vol. 168 , ( 5 ) 887 - 921 .
Oliva P, Steila S ( 2016 ) . A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem .
BORGES OLIVA P, Powell T ( 2015 ) . A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis . Gentzen's Centenary The Quest for Consistency , Springer
Hedges J, Oliva P, Sprits E, Winschel V, Zahn P ( 2015 ) . Higher-Order Decision Theory .
Hedges J, Oliva P, Sprits E, Winschel V, Zahn P ( 2015 ) . Higher-Order Game Theory .
ESCARDÓ M, OLIVA P ( 2015 ) . BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS . Journal of Symbolic Logic vol. 80 , ( 1 ) 1 - 28 .
OLIVA P, POWELL T ( 2014 ) . A constructive interpretation of Ramsey's theorem via the product of selection functions . Mathematical Structures in Computer Science vol. 25 , ( 8 ) 1755 - 1778 .
Escardo M, Oliva P ( 2014 ) . The Herbrand Functional Interpretation of the Double Negation Shift .
Hedges J, Oliva P, Winschel E, Winschel V, Zahn P ( 2014 ) . A Higher-order Framework for Decision Problems and Games .
Oliva P ( 2014 ) . Preface . Electronic Proceedings in Theoretical Computer Science Eptcs . vol. 164 ,
Oliva P ( 2014 ) . Proceedings Fifth International Workshop on Classical Logic and Computation .
Escardo M, Oliva P ( 2014 ) . Bar Recursion and Products of Selection Functions .
Berardi S, Oliva P, Steila S ( 2014 ) . Proving termination with transition invariants of height omega .
Arthan R, Oliva P ( 2014 ) . On Pocrims and Hoops .
Arthan R, Oliva P ( 2014 ) . On Affine Logic and Łukasiewicz Logic .
Berardi S, Oliva P, Steila S ( 2014 ) . Proving termination of programs having transition invariants of height ω . Ceur Workshop Proceedings . vol. 1231 , 237 - 240 .
Arthan R, Oliva P ( 2013 ) . (Dual) Hoops Have Unique Halving . Automated Reasoning and Mathematics , vol. 7788 , Springer Nature
Ferreira G, Oliva P ( 2012 ) . On the Relation Between Various Negative Translations . Logic, Construction, Computation , De Gruyter
Arthan R, Oliva P ( 2012 ) . Hoops, Coops and the Algebraic Semantics of Continuous Logic .
Escardo M, Oliva P ( 2012 ) . Computing Nash Equilibria of Unbounded Games . EPiC series in computing . vol. 10 , 53 - 39 .
Arthan R, Oliva P ( 2012 ) . (Dual) Hoops Have Unique Halving .
Oliva P, Powell T ( 2012 ) . On Spector's bar recursion . MATHEMATICAL LOGIC QUARTERLY vol. 58 , ( 4-5 )
Ferreira G, Oliva P ( 2012 ) . On bounded functional interpretations . ANNALS OF PURE AND APPLIED LOGIC vol. 163 , ( 8 ) 1030 - 1049 .
Escardo M, Oliva P ( 2012 ) . The Peirce translation . ANNALS OF PURE AND APPLIED LOGIC vol. 163 , ( 6 ) 681 - 692 .
Escardó M, Oliva P, Powell T ( 2011 ) . System T and the product of selection functions . Leibniz International Proceedings in Informatics Lipics . vol. 12 , 233 - 247 .
Escardo M, Oliva P ( 2011 ) . Sequential games and optimal strategies . Proceedings of the Royal Society A vol. 467 , ( 2130 ) 1519 - 1545 .
Oliva P, Arthan R, Martin U ( 2011 ) . A Hoare logic for linear systems . Formal Aspects of Computing: applicable formal methods
Oliva P, Ferreira G ( 2011 ) . Functional interpretations of intuitionistic linear logic . Logical Methods in Computer Science vol. 7 , ( 1.9 ) 1 - 22 .
Ferreira G, Oliva P ( 2011 ) . On Various Negative Translations .
Ferreira G, Oliva P ( 2010 ) . Functional Interpretations of Intuitionistic Linear Logic .
Gaspar J, Oliva P ( 2010 ) . Proof interpretations with truth . MATH LOGIC QUART vol. 56 , ( 6 ) 591 - 610 .
Escardó M, Oliva P ( 2010 ) . What sequential games, the Tychnoff theorem and the double-negation shift have in common . Conference: Mathematically Structured Functional Programming
Oliva P ( 2010 ) . Functional interpretations of linear and intuitionistic logic . INFORMATION AND COMPUTATION . vol. 208 , 565 - 577 .
Escardo M, Oliva P ( 2010 ) . Selection functions, bar recursion and backward induction . Mathematical Structures in Computer Science . Conference: Domains IX ( Brighton, UK ) from: 22/09/2008 to: 24/09/2008 , vol. 20 , 127 - 168 .
Oliva P ( 2010 ) . Functional Interpretations of Intuitionistic Linear Logic . Journal of Logic and Computation
Escardó M, Oliva P ( 2010 ) . Computational interpretations of analysis via products of selection functions . Lecture Notes in Computer Science . Conference: Computability in Europe ( Azores ) vol. 6158 , 141 - 150 .
Ferreira G, Oliva P ( 2010 ) . Confined modified realizability . Mathematical Logic Quarterly vol. 56 , ( 1 ) 13 - 28 .
Oliva P ( 2010 ) . Hybrid functional interpretations of linear and intuitionistic logic . Journal of Logic and Computation vol. 22 , ( 2 ) 305 - 328 .
Escardó M, Oliva P ( 2010 ) . The Peirce translation and the double negation shift . Lecture Notes in Computer Science . Conference: Computability in Europe ( Azores ) 151 - 161 .
Ferreira G, Oliva P ( 2009 ) . Functional Interpretations of Intuitionistic Linear Logic . LNCS . Conference: Computer Science Logic ( Coimbra, Portugal ) vol. 5771 , 3 - 19 .
Arthan R, Martin U, Mathiesen EA, Oliva P ( 2008 ) . A General Framework for Sound and Complete Floyd-Hoare Logics . ACM Transactions on Computational Logic, 11(1), 2009
Oliva P ( 2008 ) . An analysis of Godel's 'Dialectica' interpretation via linear logic . DIALECTICA vol. 62 , ( 2 ) 269 - 290 .
Hernest MD, Oliva P, Beckmann A, Dimitracopoulos C, Lowe B ( 2008 ) . Hybrid functional interpretations . LOGIC AND THEORY OF ALGORITHMS . vol. 5028 , 251 - 260 .
Oliva P, Streicher T ( 2008 ) . On Krivine's realizability interpretation of classical second-order arithmetic . FUNDAMENTA INFORMATICAE . vol. 84 , 207 - 220 .
Ferreira F, Oliva P ( 2007 ) . Bounded functional interpretation and feasible analysis . ANN PURE APPL LOGIC vol. 145 , ( 2 ) 115 - 129 .
Oliva P, Leivant D, DeQueiroz R ( 2007 ) . Computational interpretations of classical linear logic . Logic, Language, Information and Computation, Proceedings . vol. 4576 , 285 - 296 .
Oliva P ( 2007 ) . Modified realizability interpretation of classical linear logic . 22nd Annual IEEE Symposium on Logic in Computer Science, Proceedings . 431 - 440 .
Arthan R, Martin U, Mathiesen EA, Oliva P, Hinchey M, Margaria T ( 2007 ) . Reasoning about linear systems . SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS . 123 - 132 .
Oliva P ( 2006 ) . Unifying Functional Interpretations . Notre Dame Journal of Formal Logic vol. 47 , ( 2 ) 263 - 290 .
Berger U, Oliva P ( 2006 ) . Modified bar recursion . MATH STRUCT COMP SCI vol. 16 , ( 2 ) 163 - 183 .
Martin U, Mathiesen EA, Oliva P, Esik Z ( 2006 ) . Hoare logic in the abstract . COMPUTER SCIENCE LOGIC, PROCEEDINGS . vol. 4207 , 501 - 515 .
Oliva P, Beckmann A, Berger U, Lowe B, Tucker JV ( 2006 ) . Understanding and using Spector's bar recursive interpretation of classical analysis . LOGICAL APPROACHES TO COMPUTATIONAL BARRIERS, PROCEEDINGS . vol. 3988 , 423 - 434 .
Ferreira F, Oliva P ( 2005 ) . Bounded functional interpretation . ANN PURE APPL LOGIC vol. 135 , ( 1-3 ) 73 - 112 .
Myers EW, Oliva P, Guimarães K ( 1998 ) . Reporting exact and approximate regular expression matches . Lecture Notes in Computer Science . vol. 1448 , 91 - 103 .
Berger U, Oliva P, Baaz M, Friedman SD, Krajicek J ( 2005 ) . Modified bar recursion and classical dependent choice . Logic Colloquim 01, Proceedings . vol. 20 , 89 - 107 .
Kohlenbach U, Oliva P ( 2003 ) . Proof mining in L-1-approximation . ANN PURE APPL LOGIC vol. 121 , ( 1 ) 1 - 38 .
Oliva P ( 2003 ) . Polynomial-time algorithms from ineffective proofs . 18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS . 128 - 137 .
Oliva P, Kohlenbach U ( 2003 ) . Proof mining: A systematic way of analyzing proofs in mathematics . Proc. Steklov Inst. Math vol. 242 , 136 - 164 .
Oliva P ( 2002 ) . On the computational complexity of best L-1-approximation . MATHEMATICAL LOGIC QUARTERLY . vol. 48 , 66 - 77 .
Martin U, GOTTLIEBSEN H, Oliva P, Mathiesen E . Case Studies in Analogue Hardware Verification . Conference: Conference on Computer Aided Verification, 2006
Oliva P, Escardo M . Higher-order Games with Dependent Types . Theoretical Computer Science
Oliva P, Xu C . On the Herbrand Functional Interpretation . Mathematical Logic Quarterly
Oliva P . Uniform Functional Interpretations . Conference: Computability in Europe ( Lisbon ) from: 14/07/2025 to: 18/07/2025 ,
Back to Search