Dr Paulo Oliva
Reader in Mathematical Logic
Email: p.oliva@qmul.ac.uk
Telephone: +44 20 7882 5255
Room Number: Peter Landin, CS 421A
Website: http://www.eecs.qmul.ac.uk/~pbo
Office Hours: Friday 10:3013:30
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 mapreduce and monadic programming.
Web Programming (Undergraduate)
Many computer systems are now accessed through a web interface. This module provides an indepth 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 serverclient 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 nontrivial 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

BORGES OLIVA P, Steila S (2018). A direct proof of Schwichtenberg's bar recursion closure theorem. nameOfConference

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

Hedges J, Oliva P, Shprits E et al. (2016). Selection Equilibria of HigherOrder Games. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES

Oliva P, Powell T (2016). Bar recursion over finite partial functions. nameOfConference

Oliva P, Powell T (2015). A constructive interpretation of Ramsey's theorem via the product of selection functions. nameOfConference

BORGES OLIVA P, Powell T (2015). A GameTheoretic Computational Interpretation of Proofs in Classical Analysis. nameOfConference

Escardo M, Oliva P (2015). BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS. nameOfConference

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

Ferreira G, Oliva P (2012). On bounded functional interpretations. nameOfConference

Escardo M, Oliva P (2012). The Peirce translation. nameOfConference

Escardo M, Oliva P (2011). Sequential games and optimal strategies. nameOfConference

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

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

Gaspar J, Oliva P (2010). Proof interpretations with truth. nameOfConference

Escardó M, Oliva P (2010). What sequential games, the Tychnoff theorem and the doublenegation shift have in common. Mathematically Structured Functional Programming

Oliva P (2010). Functional interpretations of linear and intuitionistic logic. nameOfConference

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

Oliva P (2010). Functional Interpretations of Intuitionistic Linear Logic. nameOfConference

Ferreira G, Oliva P (2010). Confined modified realizability. nameOfConference

Oliva P (2010). Hybrid functional interpretations of linear and intuitionistic logic. nameOfConference

Arthan R, Martin U, Mathiesen EA et al. (2009). A General Framework for Sound and Complete FloydHoare Logics. nameOfConference

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

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

Hernest MD, Oliva P (2008). Hybrid functional interpretations. nameOfConference

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

Oliva P (2007). Computational interpretations of classical linear logic. nameOfConference

Oliva P (2007). Modified realizability interpretation of classical linear logic. nameOfConference

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

Oliva P (2006). Unifying Functional Interpretations. nameOfConference

Berger U, Oliva P (2006). Modified bar recursion. nameOfConference

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

Ferreira F, Oliva P (2005). Bounded functional interpretation. nameOfConference

Kohlenbach U, Oliva P (2003). Proof mining in L1approximation. nameOfConference

Oliva P (2003). Polynomialtime algorithms from ineffective proofs. nameOfConference

Oliva P (2002). On the computational complexity of best L1approximation. nameOfConference

Berardi S, Oliva P, Steila S (publicationYear). An analysis of the Podelski–Rybalchenko termination theorem via bar recursion. nameOfConference