Menu
 
Research menu
Jump to menu

Publications:  Dr Paulo Borges Oliva

Oliva P, Powell T (2017) . Bar recursion over finite partial functions.ANNALS OF PURE AND APPLIED LOGIC vol. 168, (5) 887-921.
10.1016/j.apal.2016.11.003
Hedges J, Oliva P, Shprits E et al. (2017) . Selection Equilibria of Higher-Order Games. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES (PADL 2017). Conference: PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES vol. 10137, 136-151.
10.1007/978-3-319-51676-9_9
http://qmro.qmul.ac.uk/xmlui/handle/123456789/25211
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.
10.1017/S0960129513000340
http://qmro.qmul.ac.uk/xmlui/handle/123456789/10531
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
http://qmro.qmul.ac.uk/xmlui/handle/123456789/10514
Escardo M, Oliva P (2015) . BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS.JOURNAL OF SYMBOLIC LOGIC vol. 80, (1) 1-28.
10.1017/jsl.2014.82
Oliva P, Powell T (2012) . On Spector's bar recursion.MATHEMATICAL LOGIC QUARTERLY vol. 58, (4-5)
10.1002/malq.201100106
Ferreira G, Oliva P (2012) . On bounded functional interpretations.ANNALS OF PURE AND APPLIED LOGIC vol. 163, (8) 1030-1049.
10.1016/j.apal.2011.12.025
Escardo M, Oliva P (2012) . The Peirce translation.ANNALS OF PURE AND APPLIED LOGIC vol. 163, (6) 681-692.
10.1016/j.apal.2011.11.002
Escardo M, Oliva P (2011) . Sequential games and optimal strategies.Proceedings of the Royal Society A vol. 467, (2130) 1519-1545.
10.1098/rspa.2010.0471
Oliva P, Arthan R, Martin U (2011) . A Hoare logic for linear systems.Formal Aspects of Computing: applicable formal methods
10.1007/s00165-011-0180-9
Oliva P, Ferreira G (2011) . Functional interpretations of intuitionistic linear logic.Logical Methods in Computer Science vol. 7, (1.9) 1-22.
10.2168/LMCS-7(1:9)2011
Gaspar J, Oliva P (2010) . Proof interpretations with truth.MATH LOGIC QUART vol. 56, (6) 591-610.
10.1002/malq.200910112
Escardó M, Oliva P (2010) . What sequential games, the Tychnoff theorem and the double-negation shift have in common. Conference: Mathematically Structured Functional Programming
10.1145/1863597.1863605
Oliva P (2010) . Functional interpretations of linear and intuitionistic logic. INFORMATION AND COMPUTATION. vol. 208, 565-577.
10.1016/j.ic.2008.11.008
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.
10.1017/S0960129509990351
Oliva P (2010) . Functional Interpretations of Intuitionistic Linear Logic.Journal of Logic and Computation
10.1093/logcom/exq007
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.
10.1002/malq.200810029
Oliva P (2010) . Hybrid functional interpretations of linear and intuitionistic logic.Journal of Logic and Computation vol. 22, (2) 305-328.
10.1093/logcom/exq007
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.
10.2168/LMCS-7(1:9)2011
Oliva P (2008) . An analysis of Godel's 'Dialectica' interpretation via linear logic.DIALECTICA vol. 62, (2) 269-290.
10.1111/j.1746-8361.2008.01135.x
Hernest MD, Oliva P (2008) . Hybrid functional interpretations. LOGIC AND THEORY OF ALGORITHMS. Editors: Beckmann, A, Dimitracopoulos, C, Lowe, B, vol. 5028, 251-260.
10.1007/978-3-540-69407-6_29
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.
10.1016/j.apal.2006.07.002
Oliva P (2007) . Computational interpretations of classical linear logic. Logic, Language, Information and Computation, Proceedings. Editors: Leivant, D, DeQueiroz, R, vol. 4576, 285-296.
10.1007/978-3-540-73445-1_20
Oliva P (2007) . Modified realizability interpretation of classical linear logic. 22nd Annual IEEE Symposium on Logic in Computer Science, Proceedings. 431-440.
10.1109/LICS.2007.32
Arthan R, Martin U, Mathiesen EA et al. (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.
10.1109/SEFM.2007.13
Oliva P (2006) . Unifying Functional Interpretations.Notre Dame Journal of Formal Logic vol. 47, (2) 263-290.
10.1305/ndjfl/1153858651
Berger U, Oliva P (2006) . Modified bar recursion.MATH STRUCT COMP SCI vol. 16, (2) 163-183.
10.1017/S0960129506005093
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.
10.1007/11780342_44
Ferreira F, Oliva P (2005) . Bounded functional interpretation.ANN PURE APPL LOGIC vol. 135, (1-3) 73-112.
10.1016/j.apal.2004.11.001
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.
10.1016/S0168-0072(02)00081-7
Oliva P (2003) . Polynomial-time algorithms from ineffective proofs. 18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS. 128-137.
10.1109/LICS.2003.1210052
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.
10.1002/1521-3870(200210)48:1+<66::AID-MALQ66>3.0.CO;2-Y
Arthan R, Martin U, Mathiesen EA et al.. A General Framework for Sound and Complete Floyd-Hoare Logics.ACM Transactions on Computational Logic, 11(1), 2009
10.1145/1614431.1614438
Berardi S, Oliva P, Steila S. An analysis of the Podelski–Rybalchenko termination theorem via bar recursion.Journal of Logic and Computationexv058-exv058.
10.1093/logcom/exv058
BORGES OLIVA P, Escardo M. The Herbrand Functional Interpretation of the Double Negation Shift.The Journal of Symbolic Logic
10.1017/jsl.2017.8
http://qmro.qmul.ac.uk/xmlui/handle/123456789/22039
Return to top