Three Research Positions - Foundations of Distributed Computation

[Peter Sewell <Peter.Sewell@cl.cam.ac.uk>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2978 bytes --]


[Apologies for multiple posting!]

We'd be grateful if you could draw this to the attention of any
suitable candidates - OCaml implementation expertise would be
especially welcome.  Thanks,
Peter


RESEARCH ASSOCIATE/RESEARCH ASSISTANT (THREE POSTS)
Foundations of Distributed Computation

Computer Laboratory, University of Cambridge

<http://www.cl.cam.ac.uk/users/pes20/advert2.html>

Ref No: NR60
Grade: NRAS Salary: £20,044 - £30,002 pa. 
Grade: RAST Salary: £20,044 - £22,289 pa

Limit of tenure: Up to two years for two Research Associate positions;
one year for one Research Assistant position.



Three Research Assistant/Research Associate positions are available in
the foundations of distributed computation, funded by EPSRC grants
EP/C510712 (Sewell, Gibbens, Norrish) and GR/T11715 (Sewell, Pitts).

The work spans several areas:

    * Design, semantics and implementation of programming language
       constructs for distribution - covering type-safe communication,
       naming, version change, module systems, and dynamic linking.
    * Formal specification, automated testing and proof about
       real-world network protocols.
    * Tool support for mechanisation of large semantic definitions.
    * Reasoning about executable distributed programs.

It builds on previous work on the experimental Acute programming
language, on the NetSem semantics of real-world network protocols, and
on the concerns of the POPLmark challenge problem in semantic
mechanisation. Details of all these can be found at
<http://www.cl.cam.ac.uk/users/pes20/index.html#PAPERS>.

For the two-year positions you should have a PhD in Computer Science,
with a strong background in one or more of the following:

    * Programming Language Semantics
    * Programming Language Implementation (especially with respect to OCaml)
    * Automated proof assistants (especially one or more of HOL,
       Isabelle, Coq, and Twelf).
    * Network Protocols
    * Distributed Systems

The one-year appointment may be either at the postdoctoral level
(Research Associate) as above, or at a post-graduate level (Research
Assistant). For the latter you should have a good first-class degree
in Computer Science. For a suitably experienced candidate it may be
possible to upgrade to a Senior Research Associate appointment.

Enquiries about the project should be addressed to Dr Peter Sewell,
<http://www.cl.cam.ac.uk/users/pes20/>.

To apply please send as soon as possible a letter of application
including a brief statement of the particular contribution you would
make to the project, a CV, a completed PD18 form
(<http://www.admin.cam.ac.uk/offices/personnel/forms/pd18/>) and the
names and contact details (postal and email addresses) of 2 referees to

  Kate Ellis
  University of Cambridge
  Computer Laboratory
  15 JJ Thomson Avenue
  Cambridge
  CB3 0FD
  United Kingdom

or by e-mail (with documents in PDF format) to personnel-admin@cl.cam.ac.uk.
Closing date: 20 April 2006.