Logic List Mailing Archive

PhD student positions in mathematics and theoretical computer science, Bath (U.K.), Deadline: 28 Feb 2015

We offer 3.5-year PhD positions in mathematics and theoretical computer 
science. 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).

Deadline: 28 February 2015, but applications are processed as they are 
received.

Research team:

     Mathematical Foundations of Computation
     (Proofs, Categories, Semantics, Geometry, Computer Algebra and Cryptography)
     http://www.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://www.bath.ac.uk/science/graduate-school/research-programmes/phd-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.

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) 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, 
Computer Algebra and Cryptography.