PhD Research Project: Efficient and Natural Proof Systems

Hello, could you please help us advertise the=20
following position? Ciao,   -Alessio



*** PhD Studentship ***

Research Project: Efficient and Natural Proof Systems
<http://www.cs.bath.ac.uk/ag/ENPS/>

Institution: University of Bath - Department of Computer Science

PhD Supervisors: Alessio Guglielmi and/or Guy McCusker
<http://alessio.guglielmi.name>
<http://www.cs.bath.ac.uk/~gam23/>

Application Deadline: 17 April 2013

Math is growing more complex each day, to the=20
point that the assistance of computers is=20
becoming necessary even for the most=20
theoretically inclined among the mathematicians=20
(see this recent article by Natalie Wolchover on=20
Wired: <http://is.gd/Qf2qpd>). After centuries of=20
producing proofs in our heads and then describing=20
them in papers, we are moving fast towards a=20
future of proofs conceived by humans together=20
with computers, which in turn will guarantee=20
their correctness and availability.

But what is a proof? What could a common language=20
between humans and computers be? A satisfying=20
definition of mathematical proof has proved to be=20
a very elusive concept. Suffice to say that the=20
problem of deciding whether two formal proofs are=20
the same has remained open since Hilbert=20
formulated it more than one hundred years ago.

=46inding efficient and natural proof systems is a=20
fascinating problem that spans from philosophy,=20
through math, to computer science. There is=20
growing evidence that, at its core, good=20
solutions can be provided by geometrical ideas.=20
Indeed, many mathematicians interested in the=20
foundations of mathematics have recently turned=20
to geometry.

We propose a PhD in the context of the EPSRC=20
project `Efficient and Natural Proof Systems=B4=20
(see at <http://is.gd/7XYPbt>). In this project,=20
we will define a new proof system which,=20
essentially, will represent proofs as geometric=20
shapes equivalent under continuous deformation.=20
Three areas of mathematics and theoretical=20
computer science concur in the definition of=20
these proof systems: categorical semantics, proof=20
theory and proof complexity. The result of this=20
project will be the completion of three decades=20
of efforts in proof theory that started with=20
linear logic and continued with deep inference=20
(see <http://is.gd/leM81c> [beware, there are=20
jokes in that page]).

We are looking for a brilliant mathematician or=20
theoretical computer scientist who is not afraid=20
of working with category theory and who has a=20
good geometric intuition. We provide a fully=20
funded three-year PhD position in the exceptional=20
research environment of one of the best worldwide=20
research groups in semantics and proof theory=20
(see at <http://is.gd/ZUlZ5n>).

Your full tuition fees will be covered and you=20
will receive a standard EPSRC maintenance payment=20
of =A313,726/annum (13/14 rate) for three years.=20
=46unding for this project is available to citizens=20
of a number of European countries (including the=20
UK). In most cases this will include all EU=20
nationals. However full funding may not be=20
available to all applicants and you should read=20
the full department and project details for=20
further information.

To apply, start here: <http://is.gd/RCaAvA/>.=20
=46eel free to contact Alessio Guglielmi for any=20
question you might have about this position.