[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
** PhD position in proof theory at the University of Bath
EFFICIENT AND NATURAL PROOFS AND ALGORITHMS
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 answering them will
enable technological advances of great impact on 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.
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/>.
Our group is very well-financed via several grants. Thanks to our international
relations, working with us means having a multicultural experience 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.
** Supervisors and research team
Alessio Guglielmi <http://alessio.guglielmi.name>
Willem Heijltjes <http://www.cs.bath.ac.uk/~wbh22/>
<https://www.bath.ac.uk/projects/mathematical-foundations-of-computation/>
Informal enquiries are welcomed:
<mailto:a.guglie...@bath.ac.uk>
<mailto:w.b.heijlt...@bath.ac.uk>
** Application deadline: 29 March 2020.
** Anticipated start date: 28 September 2020.
** Candidate requirements
Applicants should hold, or expect to gain, a First Class or Upper Second Class
Honours degree in Mathematics or Computer Science, or the equivalent from an
overseas university. A master’s level qualification would also be advantageous.
** Funding Notes
UK and EU students who have been ordinarily resident in the UK since September
2017 will be considered for an EPSRC DTP studentship. Funding will cover UK/EU
tuition fees, maintenance at the UKRI Doctoral Stipend rate (£15,285 per annum,
2020/21 rate) and a training support grant of £1,000 per annum for 3.5 years.
For more information on eligibility:
<https://epsrc.ukri.org/skills/students/guidance-on-epsrc-studentships/eligibility/>.
** How to apply
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>
More information about applying for a PhD at Bath may be found at
<http://www.bath.ac.uk/guides/how-to-apply-for-doctoral-study/>
