Postdoc positions for ERC “RustBelt” project (Saarbrücken, Germany)

Message from Derek Dreyer:

I am pleased to announce the availability of 2 postdoc positions for
the project "RustBelt: Logical Foundations for the Future of Safe
Systems Programming", funded by a 2015 ERC Consolidator Grant.

This 5-year project concerns the development of rigorous formal
foundations for the Rust programming language.  The project summary
appears below.

Although the main high-level goal of the project is to build logical
foundations for the Rust programming language, the project also serves
to fund technical work on two other major research efforts that feed
into the main goal:

1. The development of *Iris*, a simplifying and unifying framework for
higher-order concurrent separation logic in Coq (see the Iris web page

2. Our ongoing study of improved semantics and logics for relaxed
memory models (see e.g. our work on GPS [OOPSLA'14, PLDI'15] and the
"promising" semantics [POPL'17]).

I am seeking exceptional candidates who are interested (and who
preferably have a proven track record) in one or more of the following

- Rust
- substructural/ownership type systems
- verification of concurrent programs
- weak/relaxed memory models
- interactive theorem proving in Coq
- compiler verification

Successful applicants will join the Foundations of Programming group,
led by me, at the Max Planck Institute for Software Systems (MPI-SWS)
in Saarbruecken, Germany.  Previous postdocs in the group have
included Andreas Rossberg, Chung-Kil Hur, Neel Krishnaswami, Aaron
Turon, and Jacques-Henri Jourdan.

*Application deadline*: MARCH 1.  If you are interested in joining the
RustBelt team and want to learn more about the project, please contact
me directly at  To apply for a postdoc position,
please submit a CV, research statement, and list of references to

For further information, see the project web page at:

Comments are closed.