U N I V E R S I T Y   O F   C A M B R I D G E

                     Department of Computer Science

                           Research Assistant

A research assistant is required to work on the project "Types for Proofs
and Programs", ESPRIT Basic Research Project 6453.  Our group is concerned
with applying and developing the generic theorem prover Isabelle.  Within
this context, the researcher will have freedom to investigate a variety of
areas: inductive data types and recursion, proof search, user interfaces,
verification, synthesis, representation of theories, etc.  Our group is
well equipped with several SPARCstations and a SPARCserver 10, all with
ample memory.

Applicants should have a sound training in theoretical computer science,
logic, or mathematics.  Previous experience with automated theorem proving
would be desirable.

The starting salary is 12,638-15,563 pounds per annum, depending upon
qualifications and experience.  The post is available from 12 March 1993
until 30 November 1993, with possible re-appointment until 31 August 1995.

Please send your application, with full curriculum vitae and the names of
two referees, to Lawrence Paulson, Computer Laboratory, University of
Cambridge, Pembroke Street, Cambridge CB2 3QG, England (Tel: 0223 334623,
Fax: 0223 334678, Internet: lcp@cl.cam.ac.uk).  Applications are due by 19
February 1993.