[TYPES/announce] ERC "RustBelt" project: Postdoc and PhD student positions available at MPI-SWS

[Derek Dreyer]

[Note: The initial deadline was October 31, but I will continue
considering applications until the end of the year.  If you are
interested, please contact me directly first.]

I am pleased to announce the availability of multiple postdoc and PhD
student positions in my research group at the Max Planck Institute for
Software Systems (MPI-SWS), funded by a 2015 ERC Consolidator Grant
for the project "RustBelt: Logical Foundations for the Future of Safe
Systems Programming".

http://plv.mpi-sws.org/rustbelt

This 5-year project (which began in April 2016) concerns the
development of rigorous formal foundations for the Rust programming
language.  The project summary appears at the bottom of this message.

Although the main high-level goal of the project is to build logical
foundations for the Rust programming language -- see our POPL'18 paper
-- 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 [POPL'15, ICFP'16,
POPL'17, ESOP'17, ICFP'18, JFP'18].  See the Iris web page at
http://iris-project.org/ for further details.

2. Our ongoing study of improved semantics and logics for relaxed
memory models (see e.g. our work on the separation logic GPS
[OOPSLA'14, PLDI'15, ECOOP'17] and the "promising" semantics for
solving the out-of-thin-air problem [POPL'17, ECOOP'17, ESOP'18]).

*POSTDOCS*: I am seeking exceptional candidates with a strong,
internationally competitive track record of research in programming
languages and/or verification.  The primary criterion is quality, but
I am particularly interested in candidates who have specialized
expertise in one or more of the following areas:

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

Experience programming in Rust is a welcome bonus, but not required.

*STUDENTS*: I am seeking exceptional candidates who have at least some
background in programming language theory and/or formal methods, and
who are eager to work on deep foundational problems with the potential
for direct impact on a real, actively developed language.  A
bachelor's or master's degree is required.  For more details about the
MPI-SWS graduate program, see here:
https://www.mpi-sws.org/graduate-studies/.

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.  Current and former postdocs in the group
have included Andreas Rossberg (co-designer of WebAssembly), Chung-Kil
Hur, Neel Krishnaswami, Aaron Turon (manager of the Rust project at
Mozilla), Jacques-Henri Jourdan, Ori Lahav, Pierre-Marie Pédrot, and
Azalea Raad.  Current and former PhD students in the group have
included Georg Neis, Beta Ziliani, Scott Kilpatrick, David Swasey,
Ralf Jung, Jan-Oliver Kaiser, Hoang-Hai Dang, Marko Doko, and
@pythonesque.  The RustBelt project benefits from longstanding active
collaborations with Viktor Vafeiadis (MPI-SWS), Lars Birkedal (Aarhus
University), Chung-Kil Hur & Jeehoon Kang (Seoul National University),
Deepak Garg (MPI-SWS), and Robbert Krebbers (TU Delft), as well as the
many contributors to the Iris project (http://iris-project.org).

The working language at MPI-SWS is English.

I will be considering applications until the end of the year.  If you
are interested in joining the RustBelt team and want to learn more
about the project, please contact me directly at dreyer at mpi-sws.org.
To apply for a postdoc (or PhD student) position, please submit a CV
(and/or grade transcript), research statement (or statement of
purpose), and list of references to https://apply.mpi-sws.org.  If you
are unable to apply by the deadline but are interested in a position,
please contact me anyway.

For further information, see the project web page at:
http://plv.mpi-sws.org/rustbelt/

Best regards,
Derek Dreyer

----------------

Summary of the RustBelt project proposal:

A longstanding question in the design of programming languages is how
to balance safety and control.  C-like languages give programmers
low-level control over resource management at the expense of safety,
whereas Java-like languages give programmers safe high-level
abstractions at the expense of control.

Rust is a new language developed at Mozilla Research that marries
together the low-level flexibility of modern C++ with a strong
"ownership-based" type system guaranteeing type safety, memory safety,
and data race freedom.  As such, Rust has the potential to
revolutionize systems programming, making it possible to build
software systems that are safe by construction, without having to give
up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally
investigated, and it is not at all clear that they hold.  To rule out
data races and other common programming errors, Rust's core type
system prohibits the aliasing of mutable state, but this is too
restrictive for implementing some low-level data structures.
Consequently, Rust's standard libraries make widespread internal use
of "unsafe" blocks, which enable them to opt out of the type system
when necessary.  The hope is that such "unsafe" code is properly
encapsulated, so that Rust's language-level safety guarantees are
preserved.  But due to Rust's reliance on a weak memory model of
concurrency, along with its bleeding-edge type system, verifying that
Rust and its libraries are actually safe will require fundamental
advances to the state of the art.

In this project, we aim to equip Rust programmers with the first
formal tools for verifying safe encapsulation of "unsafe" code.  Any
realistic languages targeting this domain in the future will encounter
the same problem, so we expect our results to have lasting impact.  To
achieve this goal, we will build on recent breakthrough developments
by the PI and collaborators in concurrent program logics and semantic
models of type systems.