[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
We are recruiting for 2 PhD positions
Funding: Competition funded
Deadline: Monday 16 May 2022
Start: October 2022 (anticipated)
Contacts:
Willem Heijltjes [email protected]
Alessio Guglielmi [email protected]
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/research-groups/mathematical-foundations-of-computation/__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20Nectr4_$
Please see at the end of this email for a list of projects and supervisors.
===== How to apply =====
To apply, please complete the following online form:
https://urldefense.com/v3/__https://samis.bath.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app&code1=RDUCM-FP01&code2=0016__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20MasVTIB$
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!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20Lx3hym9$
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 | [email protected] |
https://urldefense.com/v3/__http://people.bath.ac.uk/masrjb/__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20BOBjs4C$
James Davenport | [email protected] |
https://urldefense.com/v3/__http://people.bath.ac.uk/masjhd/__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20Akrtr7S$
Tom Powell | [email protected] |
https://urldefense.com/v3/__http://t-powell.github.io__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20EvuXGzT$
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!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20L4g0Znm$
) 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 | [email protected] |
https://urldefense.com/v3/__http://alessio.guglielmi.name__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20MblPkkG$
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 | [email protected] |
https://urldefense.com/v3/__http://willem.heijltj.es__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20NHgzHto$
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 | [email protected] |
https://urldefense.com/v3/__http://www.cs.bath.ac.uk/*jl317/__;fg!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20IeoDZ4w$
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 | [email protected] |
https://urldefense.com/v3/__http://www.cs.bath.ac.uk/*gam23/__;fg!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20O2KJGii$
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 | [email protected] |
https://urldefense.com/v3/__http://t-powell.github.io__;!!IBzWLUs!XU1FULh3w8KnDha7nWYXGf08MMM-71LNQcr-DhHrrtz91Y-SmzHGanKIhGuuxHC_bJazbpZcrv3lyvF9aETm7DJjIsEQSPM20EvuXGzT$
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.
