PhD positions from October 2016 at the University of Bath

The Department of Computer Science of the University of Bath is offering =
several fully funded PhD studentships for an October 2016 start.

An illustrative PhD project in proof theory is outlined below. Up to =
three studentships are available for this project. Applicants should =
have or expect to gain at least the equivalent of a 2.1 BSc/MSc in a =
relevant subject area and must satisfy RCUK residency rules for the full =
studentship (fees + stipend):

 https://www.epsrc.ac.uk/skills/students/help/eligibility/

Deadline: 5 March 2016, but studentships might be allocated before the =
deadline.

Research team: Mathematical Foundations (Proofs, Categories, Semantics, =
Geometry and Computer Algebra)

  http://www.bath.ac.uk/comp-sci/research/mathematical-foundations/

To apply:

 =
http://www.bath.ac.uk/science/graduate-school/research-programmes/how-to-a=
pply/how-to-apply-computer-science.html

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. 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.

You can find more information at

  http://alessio.guglielmi.name/res/cos/
  http://www.cs.bath.ac.uk/ag/ENPS/

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.

To obtain more information and to apply, please follow the link above. =
Feel free to contact Alessio Guglielmi (A.Guglielmi AT Bath.Ac.UK).