[FOM] Interactive theorem proving: 3 Postdoctoral positions at Cambridge

[Lawrence Paulson]

ALEXANDRIA is a five-year ERC-funded project aimed at making interactive theorem proving useful in mathematical research. The workplan includes pilot studies to identify critical issues, library development and the implementation of advanced search, perhaps using machine learning. Two mathematicians and an Isabelle architect will be hired. Official descriptions of the vacancies are online:

http://www.jobs.cam.ac.uk/job/13866/
http://www.jobs.cam.ac.uk/job/13867/

We can look forward to some exciting developments! And while this project will be based on Isabelle, I also hope for fruitful cooperation with users of other systems.

Larry Paulson

Computer Laboratory, University of Cambridge
Cambridge CB3 0FD, England
Tel: +44(0)1223 334623   








Larry