Research Associate In Generic Theorem Proving

To: types@theory.LCS.MIT.EDU
Subject: Research Associate In Generic Theorem Proving
From: lcp%computer-lab.cambridge.ac.uk@nss.cs.ucl.ac.uk
Date: Wed, 15 Feb 89 14:43:11 EST
Sender: meyer@theory.LCS.MIT.EDU

Date: Wed, 15 Feb 89 18:20:18 GMT

To: TYPES@theory.LCS.MIT.EDU, info-hol%clover.ucdavis.edu@nss.cs.ucl.ac.uk,
        rewriting-list%crin.crin.fr@nss.cs.ucl.ac.uk,
        theorem-provers@mc.lcs.mit.edu

			  UNIVERSITY OF CAMBRIDGE
			    Computer Laboratory

	       RESEARCH ASSOCIATE IN GENERIC THEOREM PROVING

The University hopes to be in a position to appoint a Research Associate
for 30 months to work on the ESPRIT Basic Research Action entitled "Logical
Frameworks: Design, Implementation, and Experiment".  The project aims to
develop theorem proving methods that uniformly handle many logics.  The
other sites in the project are INRIA (Rocquencourt and Sophia-Antipolis
laboratories), and the Universities of Edinburgh, Manchester, Oxford,
Turin, Paris VII, and Chalmers University in Sweden.

At Cambridge, the generic theorem prover Isabelle has been operational
since 1986.  Isabelle currently supports several first-order logics,
Constructive Type Theory, higher-order logic, and Zermelo-Fraenkel set
theory.

The Research Associate would be to do any kind of work in this area.
Examples: notions of `parametric theory' suitable for Generic Theorem
Proving; the formalization of a body of mathematics (or program
specifications) using Isabelle; logics for program synthesis; improvements
to Isabelle itself.

Cambridge has long experience with building theorem provers and using them
to verify hardware and software.  For example, Gordon's HOL has been used to
verify microprocessors.

To apply, please send curriculum vitae with the names of two referees to
Lawrence Paulson, Computer Laboratory, Pembroke Street, Cambridge CB2 3QG,
England.  Phone: (0223) 334623, EMAIL: lcp@cl.cam.ac.uk.  The applicant
should have a broad knowledge of logic, functional programming, or
verification techniques.  

The project details are still being negotiated.  We expect a starting date
between April and August 1989.  Salary is on the 1A scale, up to 14,500
pounds depending on age and experience.