Dr Paulo OlivaReader in Mathematical LogicEmail: p.oliva@qmul.ac.ukTelephone: +44 20 7882 5255Room Number: Peter Landin, CS 421AWebsite: http://www.eecs.qmul.ac.uk/~pboOffice Hours: Friday 11:00-13:00ProfileTeachingResearchPublicationsProfileI 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.TeachingFunctional 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.ResearchResearch 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