[isabelle] postdoc available


Salary range:   £19,460 - £29,127

Length of appointment:   Up to 15 Months

A postdoctoral Research Associate post is available in the area of automated reasoning at the Computer Laboratory, University of Cambridge. The research concerns linking interactive proof tools (such as Isabelle) to resolution theorem provers (such as Vampire or SPASS) that are running in the background. The objective is to give the interactive tool greatly improved automation. Part of the work involves programming, to manage the background processes and to integrate the tools. However, the main part of the work concerns logical problems, such as reconciling the differences between higher- order logic and first-order logic, and translating resolution proofs into natural deduction proofs. The Research Associate will work alongside the Principal Investigator and a research student.

Applicants should hold, or be about to complete, a PhD in computer science, or have equivalent research experience. They should have expertise with programming in ML and with formal proof tools. Knowledge of thread programming (in any language) would be most valuable. Detailed information concerning the project is available at the URL www.cl.cam.ac.uk/users/lcp/Grants/ automation.html

Applications should include a completed PD18 form http:// www.admin.cam.ac.uk/offices/personnel/forms/pd18/, the name, address and email address of three referees and include a copy of a recent publication. Applications should be submitted by 14th October 2005 to Professor Lawrence C. Paulson, Computer Laboratory, Cambridge CB3 0FD. E-mail: Larry.Paulson at cl.cam.ac.uk

Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
15 JJ Thomson Avenue, Cambridge CB3 0FD, England
Tel: +44(0)1223 334623    Fax: +44(0)1223 334678

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.