[TYPES/announce] Postdoc position in Applied Semantics for Production Architectures

[Peter Sewell]

[please circulate this to any likely candidates - thanks, Peter]

Research Associate/Senior Research Associate in Applied Semantics for
Production Architectures

University of Cambridge Computer Laboratory
Research Associate £29,301 - £38,183 or Senior Research Associate £39,324 -
49,772
Fixed-term: until February 28, 2019, when the grant funding the post
currently ends.
Details: http://www.jobs.cam.ac.uk/job/12397/


Do you want to help build mathematically rigorous foundations for
real-world computing, to make it more robust and secure?

We have an ongoing project to establish rigorous semantic models for
production multiprocessors, to provide a clear basis for programming,
software verification, and hardware verification. This involves long-term
close collaborations with ARM and IBM, and we have an agreement with ARM to
take their internal ISA description, build a mathematical model based on
it, integrate it with the concurrency semantics we are developing, and
release the whole in a form usable for verification. This will provide the
first strongly validated public model for a production multiprocessor
architecture. We also have a close collaboration with the CHERI research
project, developing processors with hardware-accelerated in-process memory
protection and sandboxing, together with an open-source operating system
and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the
heart of the CHERI design process. For more details, see some of our
previous papers:
POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (
http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (
http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (
http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf), CHERI
ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html), CHERI (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (
http://rems.io).

We have a position available to work on:

- the development of our Sail metalanguage for ISA description: a language
with a lightweight dependent type system, designed to capture ARM, IBM
POWER, and CHERI instruction semantics in an engineer-friendly way;
- translation from Sail to generate efficient emulators and usable
theorem-prover definitions;
- mechanised proof about the architecture definitions, e.g. of security
properties, relationships between concurrency models, and correctness
results for high-level language concurrency compilation; and/or
- development of reasoning, symbolic execution, debugging, and/or
model-checking tools above the architecture definitions - the initial work
should generate many opportunities along these lines.

The successful candidate must have a PhD (or equivalent experience), a
track-record of publication in relevant areas of Computer Science, good
knowledge of English and communication skills, and the expertise and
commitment to apply rigorous semantics to real systems. We're looking for
people with the skills to make solid models and tools, well-engineered and
widely usable. You should have expertise in one or more of:

- functional programming (e.g. OCaml)
- programming language semantics and type systems
- theorem provers, especially Isabelle and/or Coq
- symbolic execution
- model-checking

For senior applicants, e.g. who will be able to contribute substantially to
future grant applications, it may be possible to appoint at the Senior
Research Associate level.

This is part of the broader REMS (Rigorous Engineering for Mainstream
Systems) programme grant: a lively collaboration between systems and
semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and
apply mathematically rigorous semantics to mainstream systems.

Informal enquiries should be directed to Peter Sewell (
Peter.Sewell at cl.cam.ac.uk).

To apply online for this vacancy, please click on the 'Apply' button below.
This will route you to the University's Web Recruitment System, where you
will need to register an account (if you have not already) and log in
before completing the online application form.

Please ensure you upload your Curriculum Vitae (CV) and a cover letter
explaining your potential contribution to the project, as pdf documents.
Include the names of 2 or 3 referees at the appropriate point in the online
application. Your referees should be prepared to send references within a
week of the closing date, if asked by the University. If you upload any
additional documents which have not been requested, we will not be able to
consider these as part of your application.

Please quote reference NR10978 on your application and in any
correspondence about this vacancy.

The University values diversity and is committed to equality of opportunity.

The University has a responsibility to ensure that all employees are
eligible to live and work in the UK.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20161215/0effa8ba/attachment-0001.html>