Publications: Dr Paulo Oliva
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
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, Powell T(2015).
A constructive interpretation of Ramsey's theorem via the product of selection functions. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
vol. 25,
(8)
1755-1778.
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
Escardo M, Oliva P(2015).
BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS. JOURNAL OF SYMBOLIC LOGIC
vol. 80,
(1)
1-28.
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.
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.
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.
Arthan R, Martin U, Mathiesen EA, Oliva P(2009).
A General Framework for Sound and Complete Floyd-Hoare Logics. ACM Transactions on Computational Logic
vol. 11,
(1)
1-31.
Ferreira G, Oliva P (2009).
Functional Interpretations of Intuitionistic Linear Logic. LNCS.
Conference: Computer Science Logic
(Coimbra, Portugal)
vol. 5771,
3-19.
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.
Ferreira F, Oliva P(2005).
Bounded functional interpretation. ANN PURE APPL LOGIC
vol. 135,
(1-3)
73-112.
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.
