Menu
 
Research menu
Jump to menu

Publications:  Dr Paulo Oliva

BORGES OLIVA P, Steila S(2018). A direct proof of Schwichtenberg's bar recursion closure theorem. The Journal of Symbolic Logic
10.1017/jsl.2017.33
http://qmro.qmul.ac.uk/xmlui/handle/123456789/22422
BORGES OLIVA P, Escardo M(2017). 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
Hedges J, Oliva P, Shprits E et al.. 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(2016). Bar recursion over finite partial functions. ANNALS OF PURE AND APPLIED LOGIC vol. 168, (5) 887-921.
10.1016/j.apal.2016.11.003
http://qmro.qmul.ac.uk/xmlui/handle/123456789/31912
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
Berardi S, Oliva P, Steila S(2015). An analysis of the Podelski–Rybalchenko termination theorem via bar recursion. Journal of Logic and Computationexv058-exv058.
10.1093/logcom/exv058
http://qmro.qmul.ac.uk/xmlui/handle/123456789/31913
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
http://qmro.qmul.ac.uk/xmlui/handle/123456789/31924
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.
Arthan R, Martin U, Mathiesen EA et al.(2009). A General Framework for Sound and Complete Floyd-Hoare Logics. ACM Transactions on Computational Logic vol. 11, (1) 1-31.
10.1145/1614431.1614438
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
Return to top