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 ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
