Fixed-term: The funds for this post are available for 5 years.
The Computer Laboratory is seeking two post-doctoral Research Associates to join a project concerned with the formalisation of mathematics within Isabelle/HOL and with the management of large formalised libraries of mathematics. The project is entitled ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician.
Interactive theorem provers, such as Coq, HOL Light and Isabelle, have been successfully used to formalise significant bodies of mathematics, notably in analysis. Moreover, there is a growing awareness among mathematicians that this technology has the potential to become useful in mathematics research. Unfortunately, existing libraries of formalised mathematics are incomplete and cryptic, and existing technology is a poor fit to standard mathematical practice. ALEXANDRIA seeks to address this situation.
The ideal candidates for this position
Should have a strong background in mathematics (preferably a PhD)
Should have some exposure to interactive theorem proving
Should have a PhD in a relevant subject area (or be very close to submitting their PhD).
The project plan includes pilot studies to formalise some research-level mathematics in Isabelle/HOL in order to identify key issues. Other possible tasks include extending and organising Isabelle's existing libraries systematically to provide full coverage of core undergraduate mathematics. The full project proposal is available here: http://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/Part-B2.pdf
The position is funded by a 2.4M Euro grant from the ERC, led by Professor Lawrence C. Paulson FRS, to whom enquiries should be addressed: http://www.cl.cam.ac.uk/~lp15/
Start date: as soon as possible after 1st September 2017
To apply online for this vacancy, please click on the 'Apply' button below. This will route you to the University's Web Recruitment System, where you will need to register an account (if you have not already) and log in before completing the online application form.
Please ensure you upload your Curriculum Vitae (CV) and a brief letter explaining what you can contribute to the project. If you upload any additional documents which have not been requested, we will not be able to consider these as part of your application.
Please quote reference NR12315 on your application and in any correspondence about this vacancy.
The University values diversity and is committed to equality of opportunity.
The University has a responsibility to ensure that all employees are eligible to live and work in the UK.