[TYPES/announce] PhD positions in Mathematical Foundations of Computer Science - Bath - deadline 4 March

[Willem Heijltjes]

We are recruiting for 2 PhD positions

    Funding:  Competition funded
    Deadline: Friday 4 March 2022
    Start:    October 2022 (anticipated)
    Contacts:

        Willem Heijltjes    W.B.Heijltjes at bath.ac.uk
        Alessio Guglielmi   A.Guglielmi at bath.ac.uk

    Mathematical Foundations Group
    Department of Computer Science
    University of Bath


===== The Mathematical Foundations group =====

Our group explores some of the deepest topics in logic and their relation to the theory of computation. We establish bridges between proof theory, category theory, semantics and complexity, so that the methods of each discipline enrich the others. We design new theories and solve old problems. For example, we defined a new proof formalism, called 'open deduction', that allowed us to describe one of the most efficient known notions of computation for the lambda-calculus. That was made possible by introducing ideas from complexity theory and category theory into proof theory and its computational interpretations.

Our research programme, in a nutshell, is to help develop the mathematics of computation. This matters at least for two reasons. The first is that computing, at present, is art, not engineering. Indeed, because of the lack of mathematics, software correctness is not guaranteed the same way a bridge is guaranteed to stand, for example. The second reason is that the theory of computation is rapidly becoming one of the most important intellectual achievements of civilisation. For example, it is now helping physics and biology create new models in their domain. Because of all that, our doctoral graduates have embarked on excellent academic careers in some of the most intellectually rewarding and innovative branches of research, and will continue to do so.

Our webpage:

    https://urldefense.com/v3/__https://www.bath.ac.uk/projects/mathematical-foundations-of-computation/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3tywO-43g$ 

Please see at the end of this email for a list of projects and supervisors.



===== How to apply =====

To apply, please send a CV and transcript to one of the contacts:

    Willem Heijltjes    W.B.Heijltjes at bath.ac.uk
    Alessio Guglielmi   A.Guglielmi at bath.ac.uk

We recommended to contact us informally first, or to contact one of the supervisors of the projects at the end of this email. Please use the above contacts also for any questions.

Applicants should hold, or expect to gain, a First Class or good Upper Second Class Honours degree in Mathematics or Computer Science, or the equivalent from an overseas university. A Master’s level qualification would be advantageous. Non-UK applicants will also be required to have met the English language entry requirements of the University of Bath:

    https://urldefense.com/v3/__http://www.bath.ac.uk/corporate-information/postgraduate-english-language-requirements-for-international-students/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3sA8_Jw0A$ 

Anticipated start date: Monday 3 October 2022



===== Funding =====

Candidates applying for this project may be considered for a 3.5-year studentship from the Engineering and Physical Sciences Council (EPSRC DTP). Funding covers tuition fees, a stipend (£15,609 per annum, 2021/22 rate) and research/training expenses (£1,000 per annum). EPSRC DTP studentships are open to Home students, and a limited number of opportunities are available to excellent International candidates.



===== Projects and Supervisors =====


VERIFICATION FOR REAL POLYNOMIAL ARITHMETIC

Russell Bradford  |  R.J.Bradford at bath.ac.uk   |  https://urldefense.com/v3/__http://people.bath.ac.uk/masrjb/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3uOsAYPAA$ 
James Davenport   |  J.H.Davenport at bath.ac.uk  |  https://urldefense.com/v3/__http://people.bath.ac.uk/masjhd/__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3vY7opZDA$ 
Tom Powell        |  trjp20 at bath.ac.uk         |  https://urldefense.com/v3/__http://t-powell.github.io__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3spNE1KdA$ 

Many problems in building verified software systems in the real world (e.g. air traffic control) involve the proof of statements about real polynomial arithmetic, often including inequalities. In principle we have known how to solve such systems for many years, but the theoretical, and too often the practical, complexity is excessive.  There has been much work, at Bath, Coventry and elsewhere, in reducing the cost for important special cases, notably the cases when there are equations as well as inequalities. However, this leads to a large piece of software, resting on fairly complicated theorems.
 
Recent research by Bath, Coventry and RWTH has produced a method (https://urldefense.com/v3/__http://arxiv.org/abs/2004.04034__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3vSpgzw8g$ ) which converts such a problem into a sequence of simpler statements, which may be much easier to verify with a more conventional theorem prover. This has yet to be checked in practice, which is the goal of this project. As a PhD student, you would be working alongside the joint Bath-Coventry EPSRC-funded project, which would provide several colleagues and a large software base to start from.



NEW FOUNDATIONS OF PROOF THEORY FROM A NOVEL NOTION OF SUBSTITUTION

Alessio Guglielmi  |  A.Guglielmi at bath.ac.uk  |  https://urldefense.com/v3/__http://alessio.guglielmi.name__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3sqqHSFJw$ 

What is a proof? What is an algorithm? We understand much of WHAT can be proved and computed but we do not have yet a good theory of HOW this is done. For example, we cannot say when two given proofs or algorithms are the same, in the sense that they prove or compute something using the same method. It is a somewhat embarrassing problem to have, given that, in most branches of mathematics, we can compare objects. For instance, we can reduce two polynomials to some canonical form, like maximal factorisation, and use that for a comparison.

The source of the problem is the languages in which proofs and algorithms are represented because they model their underlying mathematical structure. In traditional proof theory, the mathematical properties of those structures are too poor. To address the problem, for the past two decades we have been building a new proof theory, called 'deep inference', whose emphasis is in HOW proofs, and by extension algorithms, are composed. That requires new languages and new design principles. One current focus of research is developing a notion of substitution for proofs, which, among other properties, should enable a powerful form of factorisation. We propose PhD projects contributing to this effort. These are foundational problems for proof theory, meaning that talent for algebra and combinatorics is more important than knowledge of logic.



A NEW APPROACH TO COMPUTATIONAL EFFECTS IN LAMBDA-CALCULUS

Willem Heijltjes  |  W.B.Heijltjes at bath.ac.uk  |  https://urldefense.com/v3/__http://willem.heijltj.es__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3vvpjrtEg$ 

A key property of the lambda-calculus, as a model of computation, is confluence: it means that we can reason about the *outcome* of a computation separately from the *process*; in other words, we can separate the *denotational* from the *operational*. When computational effects are introduced, as would be essential for a real-world functional programming language, confluence is however lost, and the outcome of a computation becomes dependent on the chosen reduction strategy.

In this project we are working with a new way of incorporating effects into the lambda-calculus: the Functional Machine Calculus. Rather than adding new primitives, we decompose the existing constructs of the lambda-calculus, which can then be used to encode various imperative features such as sequencing, state update and retrieval, and input and output. The approach preserves confluence and gives a new way of typing computational effects, which opens up new denotational and operational perspectives. As a PhD student, you would contribute to the development and extension of this promising new paradigm. Your work would draw on ideas from type theory, proof theory including deep inference and categorical logic, and denotational semantics as well as lambda calculus.



QUANTITATIVE GAME SEMANTICS

Jim Laird  |  J.D.Laird at bath.ac.uk  |  https://urldefense.com/v3/__http://www.cs.bath.ac.uk/*jl317/__;fg!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3sul-ZgwA$ 

Denotational semantics builds abstractions of computer programs and concurrent systems, which allows us to look past their syntax and represent them using mathematical structures from a range of fields such as algebra and topology. These come with powerful theorems and techniques which we can use to prove that programs and protocols are correct, secure and efficient.
  
Moving beyond binary properties: “Does this program terminate?” “Might it deadlock?” to quantitative ones: “What is its evaluation cost in time or space?” “What is the probability of returning a value?” requires models which can capture program behaviour - on which these properties depend - in a way which is abstract, structured and precise. 
Game semantics provides such a representation by modelling computation as a two-player game between a program or agent and its environment. It is intuitively appealing and has profound connections with fields from category theory to automata theory.  
This project will use these connections to investigate the relationship between games and quantitative properties of programs, and use these foundations to build new models and discover new theories.  



INTERSECTION-TYPE SEMANTICS OF IMPERATIVE PROGRAMMING

Guy McCusker  |  G.A.McCusker at bath.ac.uk  |  https://urldefense.com/v3/__http://www.cs.bath.ac.uk/*gam23/__;fg!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3uft8gSDA$ 

Imperative programming offers fast programs and fine control over execution, but is hard to verify, mainly due to the difficulty of giving a good semantics. In this project you would investigate a new approach based on intersection types, expressed in open deduction.

Intersection types can be seen from a programming-language perspective as a type system, providing static information about program behaviour, and from a semantic perspective as a presentation of a relation-based mathematical model of programs and proofs. The novelty of this project is to use non-commutative types to model sequential computation. Expressing such types effectively is made possible by the open-deduction formalism, an approach to proof theory that can alternatively be viewed as a presentation of category-theory-based semantics. The project builds on our recent work exploring intersection types in this proof formalism. A background that includes lambda-calculus or category theory would help you make a good start on it.



PROOF MINING: ALGORITHMS FROM PROOFS IN MATHEMATICS

Tom Powell  |  trjp20 at bath.ac.uk  |  https://urldefense.com/v3/__http://t-powell.github.io__;!!IBzWLUs!B24Jyxw15VSJgw-v_VH0JaxgceQy5Wtbz1usOV0PPyIr5aVgAbduvA1PDvzqpn5C41ouV3spNE1KdA$ 

Many mathematical theorems are based on the statement that something exists. For example, Euclid's theorem on the infinitude of prime numbers says that for any number N there exists some prime number p greater than N. For such statements it is natural to ask: Can we produce an algorithm for computing the thing that we claim to exist? The proof of Euclid's theorem implicitly contains an algorithm* for finding the next prime number, and we call such proofs "constructive". Unfortunately, Turing's famous discovery that the Halting problem is undecidable highlights the fact that not all proofs are constructive, and that in general one cannot always produce algorithms for witnessing existential statements. After all, for any Turing machine M on input u there exists a boolean truth value which tells us whether or not it halts, but a general algorithm which on inputs M and u returns such a boolean is not possible by Turing's result.

The question of whether or not we can produce an algorithm for a given existential theorem is complex, and requires a deep understanding of the nature of mathematical proofs as objects in their own right. The last 20-30 years has seen the growth of an exciting research area - colloquially known as "proof mining" - which addresses this question and explores the limits of what is algorithmically possible in mathematics. It turns out that by applying techniques from proof theory, it is often possible to obtain surprising algorithms from proofs that appear to be nonconstructive. In the process, one is typically required to tackle more general challenges, such as "how should mathematical objects be represented?" and "what is the fundamental structure of this proof?", and the end result is often an abstract framework which generalises and unifies classes of mathematical theorems.

Proof mining has already achieved impressive results several areas of mathematics, including functional analysis, ergodic theory and commutative algebra. As a PhD student, you would explore developing this research program in a new direction.

*Take the number N! + 1, which is not divisible by any number from 2 to N, and search for its smallest prime factor, which must therefore by greater than N.