Dr Paulo Oliva

Profile

I am a computer scientist with a PhD in Theoretical Computer Science. I am currently a Reader in Mathematical Logic, with expertise in System Verification, Game Theory, Formal Logic, and Constructive Mathematics.

Teaching

Functional Programming (Postgraduate)

Practical introduction to functional programming for students with good programming ability but no prior knowledge of FP

Functional Programming (Undergraduate)

Recent approaches to systems programming frequently involve functional programming either overtly in the sense that they use modern functional programming languages for rapid prototyping, or more covertly in that they use techniques developed in the functional setting as a way of lending greater structure and clarity to code. This module gives a structured introduction to programming in modern industrial functional languages such as Haskell and F# and to techniques such as map-reduce and monadic programming.

Web Programming (Undergraduate)

Many computer systems are now accessed through a web interface. This module provides an in-depth and practical study of techniques for programming the web. Students will become proficient in a modern web development framework using PHP for sever programming and Javascript for client programming. The strengths and weaknesses of the framework are evaluated considering issues including authentication, security, session management, cross languages (PHP, SQL, Javascript) consistency and abstraction of the server-client interface. Different architecture styles are compared, including REST and AJAX and the use of JSON. Techniques for testing and for engineering web systems that behave robustly under high load are also covered.

Research

Research Interests:

My main area of research is in mathematical logic and proof theory. In particular, I am interested in the computational content of mathematical proofs. What do theorems tell us, apart from the truth they convey? How can proofs be viewed as programs, so as to be executed, and how can programs be viewed as proofs, so that their correctness can be automatically checked? These questions become highly non-trivial when proofs involve classical logic, induction and analytical principles such as countable choice and WKL.

Recently, I have also been working on the application of formal verification to the domain of continuous systems. More precisely, developing 'Hoare logic' systems in order to prove properties of systems in the continuous time domain.

My early research career was on the topic of algorithms. That was the time when I was taking part in the ACM ICPC (International Collegiate Programming Challenge). My first paper was on pattern matching algorithms, jointly written with K. Guimaraes and E. W. Myers.

Publications

• Escardó M, Oliva P (2023). Higher-order games with dependent types. nameOfConference

  
  

  DOI: 10.1016/j.tcs.2023.114111

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/89899
• Arthan R, Oliva P (2021). On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem. nameOfConference

  
  

  DOI: 10.4115/jla.2021.13.6

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/89898
• Oliva P, Zahn P (2021). On rational choice and the representation of decision problems. nameOfConference

  
  

  DOI: 10.3390/g12040086

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/76218
• Dinis B, Oliva P (2021). A Parametrised Functional Interpretation of Heyting Arithmetic. nameOfConference

  
  

  DOI: 10.1016/j.apal.2020.102940

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/70229
• Oliva P, Arthan R (2020). Double Negation Semantics for Generalisations of Heyting Algebras. nameOfConference

  
  

  DOI: 10.1007/s11225-020-09909-y

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/64467
• Andrew L-S, Oliva P, Robinson E (2020). Kripke Semantics for Intuitionistic Lukasiewicz Logic. nameOfConference

  
  

  DOI: 10.1007/s11225-020-09908-z

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/64072
• Oliva P, Xu C (2020). On the Herbrand functional interpretation. nameOfConference

  
  

  DOI: 10.1002/malq.201900067

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/62083
• Oliva P, Arthan R (2019). Studying Algebraic Structures Using Prover9 and Mace4. nameOfConference

  
  

  DOI: 10.1007/978-3-030-28483-1_5

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/61310
• Berardi S, Oliva P, Steila S (2019). An analysis of the Podelski-Rybalchenko termination theorem via bar recursion. nameOfConference

  
  

  DOI: 10.1093/logcom/exv058

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/31913
• BORGES OLIVA P, Steila S (2018). A direct proof of Schwichtenberg's bar recursion closure theorem. nameOfConference

  
  

  DOI: 10.1017/jsl.2017.33

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/22422
• Hedges J, Oliva P, Shprits E et al. (2017). Higher-Order Decision Theory. nameOfConference

  
  

  DOI: 10.1007/978-3-319-67504-6_17

  
  

  QMRO: qmroHref
• BORGES OLIVA P, Escardo M (2017). The Herbrand Functional Interpretation of the Double Negation Shift. nameOfConference

  
  

  DOI: 10.1017/jsl.2017.8

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/22039
• Hedges J, Oliva P, Shprits E et al. (2016). Selection Equilibria of Higher-Order Games. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES

  
  

  DOI: 10.1007/978-3-319-51676-9_9

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/25211
• Oliva P, Powell T (2016). Bar recursion over finite partial functions. nameOfConference

  
  

  DOI: 10.1016/j.apal.2016.11.003

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/31912
• BORGES OLIVA P, Powell T (2015). A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis. nameOfConference

  
  

  DOI: 10.1007/978-3-319-10103-3_18

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/10514
• ESCARDÓ M, OLIVA P (2015). BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS. nameOfConference

  
  

  DOI: 10.1017/jsl.2014.82

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/31924
• OLIVA P, POWELL T (2015). A constructive interpretation of Ramsey's theorem via the product of selection functions. nameOfConference

  
  

  DOI: 10.1017/s0960129513000340

  
  

  QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/10531
• Oliva P (2014). Preface. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Oliva P (publicationYear). Proceedings Fifth International Workshop on Classical Logic and Computation. nameOfConference

  
  

  DOI: 10.4204/eptcs.164.0

  
  

  QMRO: qmroHref
• Berardi S, Oliva P, Steila S (2014). Proving termination of programs having transition invariants of height ω. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Arthan R, Oliva P (2013). (Dual) Hoops Have Unique Halving. nameOfConference

  
  

  DOI: 10.1007/978-3-642-36675-8_9

  
  

  QMRO: qmroHref
• Ferreira G, Oliva P (2012). On the Relation Between Various Negative Translations. nameOfConference

  
  

  DOI: 10.1515/9783110324921.227

  
  

  QMRO: qmroHref
• Oliva P, Powell T (2012). On Spector's bar recursion. nameOfConference

  
  

  DOI: 10.1002/malq.201100106

  
  

  QMRO: qmroHref
• Ferreira G, Oliva P (2012). On bounded functional interpretations. nameOfConference

  
  

  DOI: 10.1016/j.apal.2011.12.025

  
  

  QMRO: qmroHref
• Escardo M, Oliva P (2012). The Peirce translation. nameOfConference

  
  

  DOI: 10.1016/j.apal.2011.11.002

  
  

  QMRO: qmroHref
• Escardó M, Oliva P, Powell T (2011). System T and the product of selection functions. nameOfConference

  
  

  DOI: 10.4230/LIPIcs.CSL.2011.233

  
  

  QMRO: qmroHref
• Escardo M, Oliva P (2011). Sequential games and optimal strategies. nameOfConference

  
  

  DOI: 10.1098/rspa.2010.0471

  
  

  QMRO: qmroHref
• Oliva P, Arthan R, Martin U (2011). A Hoare logic for linear systems. nameOfConference

  
  

  DOI: 10.1007/s00165-011-0180-9

  
  

  QMRO: qmroHref
• Oliva P, Ferreira G (2011). Functional interpretations of intuitionistic linear logic. nameOfConference

  
  

  DOI: 10.2168/LMCS-7(1:9)2011

  
  

  QMRO: qmroHref
• Ferreira G, Oliva P (publicationYear). On Various Negative Translations. nameOfConference

  
  

  DOI: 10.4204/eptcs.47.4

  
  

  QMRO: qmroHref
• Gaspar J, Oliva P (2010). Proof interpretations with truth. nameOfConference

  
  

  DOI: 10.1002/malq.200910112

  
  

  QMRO: qmroHref
• Escardó M, Oliva P (2010). What sequential games, the Tychnoff theorem and the double-negation shift have in common. Mathematically Structured Functional Programming

  
  

  DOI: 10.1145/1863597.1863605

  
  

  QMRO: qmroHref
• Oliva P (2010). Functional interpretations of linear and intuitionistic logic. nameOfConference

  
  

  DOI: 10.1016/j.ic.2008.11.008

  
  

  QMRO: qmroHref
• Escardo M, Oliva P (2010). Selection functions, bar recursion and backward induction. Domains IX

  
  

  DOI: 10.1017/S0960129509990351

  
  

  QMRO: qmroHref
• Oliva P (2010). Functional Interpretations of Intuitionistic Linear Logic. nameOfConference

  
  

  DOI: 10.1093/logcom/exq007

  
  

  QMRO: qmroHref
• Escardó M, Oliva P (2010). Computational interpretations of analysis via products of selection functions. Computability in Europe

  
  

  DOI: 10.1007/978-3-642-13962-8_16

  
  

  QMRO: qmroHref
• Ferreira G, Oliva P (2010). Confined modified realizability. nameOfConference

  
  

  DOI: 10.1002/malq.200810029

  
  

  QMRO: qmroHref
• Oliva P (2010). Hybrid functional interpretations of linear and intuitionistic logic. nameOfConference

  
  

  DOI: 10.1093/logcom/exq007

  
  

  QMRO: qmroHref
• Escardó M, Oliva P (2010). The Peirce translation and the double negation shift. Computability in Europe

  
  

  DOI: 10.1007/978-3-642-13962-8_17

  
  

  QMRO: qmroHref
• Ferreira G, Oliva P (2009). Functional Interpretations of Intuitionistic Linear Logic. Computer Science Logic

  
  

  DOI: 10.2168/LMCS-7(1:9)2011

  
  

  QMRO: qmroHref
• Arthan R, Martin U, Mathiesen EA et al. (2008). A General Framework for Sound and Complete Floyd-Hoare Logics. nameOfConference

  
  

  DOI: 10.1145/1614431.1614438

  
  

  QMRO: qmroHref
• Oliva P (2008). An analysis of Godel's 'Dialectica' interpretation via linear logic. nameOfConference

  
  

  DOI: 10.1111/j.1746-8361.2008.01135.x

  
  

  QMRO: qmroHref
• Hernest MD, Oliva P (2008). Hybrid functional interpretations. nameOfConference

  
  

  DOI: 10.1007/978-3-540-69407-6_29

  
  

  QMRO: qmroHref
• Oliva P, Streicher T (2008). On Krivine's realizability interpretation of classical second-order arithmetic. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Ferreira F, Oliva P (2007). Bounded functional interpretation and feasible analysis. nameOfConference

  
  

  DOI: 10.1016/j.apal.2006.07.002

  
  

  QMRO: qmroHref
• Oliva P (2007). Computational interpretations of classical linear logic. nameOfConference

  
  

  DOI: 10.1007/978-3-540-73445-1_20

  
  

  QMRO: qmroHref
• Oliva P (2007). Modified realizability interpretation of classical linear logic. nameOfConference

  
  

  DOI: 10.1109/LICS.2007.32

  
  

  QMRO: qmroHref
• Arthan R, Martin U, Mathiesen EA et al. (2007). Reasoning about linear systems. nameOfConference

  
  

  DOI: 10.1109/sefm.2007.13

  
  

  QMRO: qmroHref
• Oliva P (2006). Unifying Functional Interpretations. nameOfConference

  
  

  DOI: 10.1305/ndjfl/1153858651

  
  

  QMRO: qmroHref
• Berger U, Oliva P (2006). Modified bar recursion. nameOfConference

  
  

  DOI: 10.1017/S0960129506005093

  
  

  QMRO: qmroHref
• Martin U, Mathiesen EA, Oliva P (2006). Hoare logic in the abstract. nameOfConference

  
  

  DOI: 10.1007/11874683_33

  
  

  QMRO: qmroHref
• Oliva P (2006). Understanding and using Spector's bar recursive interpretation of classical analysis. nameOfConference

  
  

  DOI: 10.1007/11780342_44

  
  

  QMRO: qmroHref
• Oliva P (2006). Unifying Functional Interpretations. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Ferreira F, Oliva P (2005). Bounded functional interpretation. nameOfConference

  
  

  DOI: 10.1016/j.apal.2004.11.001

  
  

  QMRO: qmroHref
• Myers EW, Oliva P, Guimarães K (1998). Reporting exact and approximate regular expression matches. nameOfConference

  
  

  DOI: 10.1007/bfb0030783

  
  

  QMRO: qmroHref
• Berger U, Oliva P (2005). Modified bar recursion and classical dependent choice. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Kohlenbach U, Oliva P (2003). Proof mining in L-1-approximation. nameOfConference

  
  

  DOI: 10.1016/S0168-0072(02)00081-7

  
  

  QMRO: qmroHref
• Oliva P (2003). Polynomial-time algorithms from ineffective proofs. nameOfConference

  
  

  DOI: 10.1109/lics.2003.1210052

  
  

  QMRO: qmroHref
• Oliva P, Kohlenbach U (2003). Proof mining: A systematic way of analyzing proofs in mathematics. nameOfConference

  
  

  DOI: doi

  
  

  QMRO: qmroHref
• Oliva P (2002). On the computational complexity of best L-1-approximation. nameOfConference

  
  

  DOI: 10.1002/1521-3870(200210)48:1+<66::AID-MALQ66>3.0.CO;2-Y

  
  

  QMRO: qmroHref