[TYPES/announce] PhD position "Efficient and natural proofs and algorithms" at University of Bath

Willem Heijltjes willem.heijltjes at gmail.com
Fri Dec 20 05:55:43 EST 2019


We are recruiting for a PhD position "Efficient and natural proofs and algorithms"

  Funding:  Competition funded (EU/UK)
  Deadline:  9 February  2020
  Start:    28 September 2020 (anticipated)

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

  Mathematical Foundations Group
  Department of Computer Science
  University of Bath


===== Description =====

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.bath.ac.uk/projects/mathematical-foundations-of-computation/

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. For example, one of our recent PhDs, Anupam Das, has won a prestigious UKRI Future Leaders Fellowship in 2019, worth £1.5M. The facilities at the University of Bath are outstanding and the city is so beautiful that UNESCO recognises it as a World Heritage Site. 


===== Contact =====

For questions about the project or the application process, please contact us: 
  Alessio Guglielmi   A.Guglielmi at bath.ac.uk
  Willem Heijltjes    W.B.Heijltjes at bath.ac.uk


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

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. 

Formal applications should be made via the University of Bath’s online application form for a PhD in Computer Science: 

  https://samis.bath.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app&code1=RDUCM-FP01&code2=0014

Anticipated start date: 28 September 2020.


===== Funding =====

Research Council funding is available on a competition basis to Home and EU students who have been resident in the UK for 3 years prior to the start of the project. For more information on eligibility, see:

  http://epsrc.ukri.org/skills/students/guidance-on-epsrc-studentships/eligibility/

Funding will cover Home/EU tuition fees, a stipend (£15,009 per annum for 2019/2020) and a training support grant of £1,000 per annum for 3.5 years. 

Applicants classed as Overseas for tuition fee purposes are NOT eligible for funding; however, we welcome all-year-round applications from self-funded candidates and candidates who can source their own funding.






More information about the Types-announce mailing list