Publications: Dr Paulo Oliva

Escardó M, Oliva P ( 2023 ) . Higher-order games with dependent types . Theoretical Computer Science vol. 974 ,

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 .

Oliva P, Arthan R ( 2020 ) . Double Negation Semantics for Generalisations of Heyting Algebras . Studia Logica: an international journal for symbolic logic

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 ( 2020 ) . On the Herbrand functional interpretation . Mathematical Logic Quarterly vol. 66 , ( 1 ) 91 - 98 .

Oliva P, Arthan R ( 2019 ) . Studying Algebraic Structures Using Prover9 and Mace4 . Springer

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 .

BORGES OLIVA P, Steila S ( 2018 ) . A direct proof of Schwichtenberg's bar recursion closure theorem . The Journal of Symbolic Logic

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 .

BORGES OLIVA P, Powell T ( 2015 ) . A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis . Gentzen's Centenary The Quest for Consistency , Editors: Kahle, R, Rathjen, M , Springer

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 .

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 . Electronic Proceedings in Theoretical Computer Science vol. 164 ,

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

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 . On Various Negative Translations . Electronic Proceedings in Theoretical Computer Science . vol. 47 , 21 - 33 .

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 ( 2008 ) . Hybrid functional interpretations . LOGIC AND THEORY OF ALGORITHMS . Editors: Beckmann, A, Dimitracopoulos, C, Lowe, B , 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 ( 2007 ) . Computational interpretations of classical linear logic . Logic, Language, Information and Computation, Proceedings . Editors: Leivant, D, DeQueiroz, R , 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 ( 2007 ) . Reasoning about linear systems . SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS . Editors: Hinchey, M, Margaria, T , 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 ( 2006 ) . Hoare logic in the abstract . COMPUTER SCIENCE LOGIC, PROCEEDINGS . Editors: Esik, Z , vol. 4207 , 501 - 515 .

Oliva P ( 2006 ) . Understanding and using Spector's bar recursive interpretation of classical analysis . LOGICAL APPROACHES TO COMPUTATIONAL BARRIERS, PROCEEDINGS . Editors: Beckmann, A, Berger, U, Lowe, B, Tucker, JV et al. , vol. 3988 , 423 - 434 .

Oliva P ( 2006 ) . Unifying Functional Interpretations . Dagstuhl Seminar Proceedings . vol. 5021 ,

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 ( 2005 ) . Modified bar recursion and classical dependent choice . Logic Colloquim 01, Proceedings . Editors: Baaz, M, Friedman, SD, Krajicek, J , 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 .