The Coq mailing list

[Lawrence Paulson <lp15 AT cam.ac.uk>]

POSTDOCTORAL RESEARCH ASSOCIATE IN AUTOMATED REASONING
Ref No: NR 718, Salary £18,265 - £27,339 pa
Limit of tenure: 36 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 interactive 
theorem proving and preferably with functional programming. 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, the name, address 
and email address of three referees and include copies of one or two 
recent publications. Applications should be submitted by 21 October 
2003 to: Professor Lawrence C. Paulson, Computer Laboratory, Cambridge 
CB3 0FD. E-mail: Larry.Paulson AT cl.cam.ac.uk Closing date: 21 October 
2003.

The application form (PD18) is at 
http://www.admin.cam.ac.uk/offices/personnel/forms/pd18/