From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8427 Path: news.gmane.org!not-for-mail From: Alessio Guglielmi Newsgroups: gmane.science.mathematics.categories Subject: 3.5-year PhD positions from October 2015 at the University of Bath Date: Sun, 14 Dec 2014 16:47:25 +0000 Message-ID: Reply-To: Alessio Guglielmi NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 (Mac OS X Mail 7.3 \(1878.6\)) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1418586475 988 80.91.229.3 (14 Dec 2014 19:47:55 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 14 Dec 2014 19:47:55 +0000 (UTC) To: categories Original-X-From: majordomo@mlist.mta.ca Sun Dec 14 20:47:50 2014 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.127]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Y0F8r-0001ZG-3b for gsmc-categories@m.gmane.org; Sun, 14 Dec 2014 20:47:45 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:45170) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1Y0F8D-0003PO-Go; Sun, 14 Dec 2014 15:47:05 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Y0F8D-0006Wj-I8 for categories-list@mlist.mta.ca; Sun, 14 Dec 2014 15:47:05 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8427 Archived-At: 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-comp= uter-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. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]