[TYPES/announce] PhD Studentships at the University of Bath

[Alessio Guglielmi]

[Hi, types and proof theory are one of the topics we study. Could you please pass this message to your best students? Many thanks. -A.]

*** Three-year PhD Studentships from October 2014 at the University of Bath ***

Research team:
    Mathematical Foundations of Computation
    (Proofs, Categories, Semantics, Geometry and Computer Algebra)
    http://bath.ac.uk/comp-sci/research/mathematical-foundations

Institution:
    University of Bath

Potential supervisors:
    Russell Bradford   http://is.gd/Y5XgCG
    Paola Bruscoli     http://cs.bath.ac.uk/pb
    James Davenport    http://staff.bath.ac.uk/masjhd
    Alessio Guglielmi  http://alessio.guglielmi.name
    Willem Heijltjes   http://cs.bath.ac.uk/~wbh22
    Jim Laird          http://cs.bath.ac.uk/~jl317
    Guy McCusker       http://cs.bath.ac.uk/~gam23
    John Power         http://is.gd/U82foN
    Nicolai Vorobjov   http://people.bath.ac.uk/masnnv/

To apply, including information on prerequisites: 
    http://bath.ac.uk/study/pg/programmes/comp-scie-mphi

50th Anniversary Excellence Studentship for an Overseas Research Student:
    12 December 2013 is the application deadline

We offer PhD positions to brilliant graduates with an interest in mathematics and theoretical computer science.

Proofs and algorithms are everyday objects in our discipline, but they are still very mysterious. Suffice to say that we are currently unable to decide whether two given proofs or two given algorithms are the same; this is an old problem that dates back to Hilbert. Also, proofs and algorithms are intimately connected in the most famous open problem in mathematics: P vs NP.

We make progress by trying to unveil the fundamental structure behind proofs and algorithms, what we call their semantics. In other words, we are interested in the following questions:

    What is a proof?
    What is an algorithm?
    How can we define them so that they have efficient and natural semantics?

The questions above are interesting in their own right, but we note that answering them will enable technological advances of great impact on the society and the economy. For example, it will be possible to build a worldwide, universal tool for developing, validating, communicating and teaching mathematics. Also, quickly producing provably bug-free and secure software will become possible, so solving one of the most complex and important open engineering problems.

In order to understand proofs and algorithms we create new mathematics starting from proof theory and semantics and utilising, among other tools, category theory and algebraic geometry. These theories are closely related, they benefit from mutual interaction and they are well represented in our team. The methods we use are mostly discrete, algebraic and combinatorial, but there is a growing geometrical component. The recent advances which our methods are mostly based on are linear logic, game semantics and deep inference on the logic side, and regular chains, cylindrical algebraic decomposition and monotone sets on the algebra/geometry side.

Last year three new PhD students joined us, each fully covered by a scholarship, from the University of Cambridge, ETH Zurich and Université Paris VII. Our group is very well financed via several grants. Thanks to our international relations, working with us means having a truly multicultural experience together with all the researchers at the forefront of this worldwide research effort. As a result, all our graduates work and publish at the highest level. The facilities at the University of Bath are outstanding and the city is so beautiful that UNESCO recognises it as a World Heritage Site.

The best applicants who are nationals from outside the European Union will be considered for some of ten "50th Anniversary Excellence Studentships for Overseas Research Students". The scholarships cover the full overseas fee, a stipend and a training support grant for three years. In other words, if you manage to win one of these scholarships you will be able to obtain an excellent PhD and maintain yourself without the need for any extra money. To be considered you need to apply before the deadline indicated above.

There will be other scholarships, for which the deadline above does not apply, that will cover all or part of the tuition fees. The details of these scholarships will be known later in the year, but you can apply and indicate if you need financial support right now.

To obtain more information and to apply, please follow the link above and choose the PhD programme in Computer Science. Feel free to contact Alessio Guglielmi (A.Guglielmi AT Bath.Ac.UK) for any questions about a PhD in Proofs, Categories and Semantics, or contact James Davenport (J.H.Davenport AT Bath.Ac.UK) for a PhD in Geometry and Computer Algebra.