Cross-posting this on behalf of Derek, I hope this is not inappropriate
[Deadline for applications: December 31, 2019. https://apply.mpi-sws.org.]
I am pleased to announce the availability of multiple PhD student,
postdoc, and intern positions in my research group at the Max Planck
Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany.
The group's research is currently mainly centered around two
interdependent projects: RustBelt and Iris.
RustBelt (https://plv.mpi-sws.org/rustbelt) is about building the
first formal foundations for the Rust programming language -- see our
"flagship" POPL'18 paper for details
RustBelt is funded primarily by a 2015 ERC Consolidator Grant (which
ends formally in 2021), the project has spawned a range of interesting
research questions that we plan to investigate indefinitely thereafter
(thanks to generous base funding from the Max Planck Society).
Iris (https://iris-project.org/) is about building a general,
flexible framework for higher-order concurrent separation logic in
Coq. Iris began five years ago as a collaborative effort between
researchers at MPI-SWS and Aarhus University, but has since enjoyed
contributions from researchers at many other participating
institutions (including TU Delft, KU Leuven, Boston College, Inria,
CNRS, Radboud University, ITU, UIC, CMU, MIT, and BedRock Systems).
These two projects have already resulted in numerous significant
publications and mechanized proof artifacts, as well as reusable
verification tools that we are continuing to actively develop. (See
the RustBelt and Iris web pages for details.)
DOCTORAL 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. Experience
with Rust and/or Coq is a plus. For more details about the MPI-SWS
doctoral program, see here: https://www.mpi-sws.org/graduate-studies/.
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:
- substructural/ownership type systems
- verification of concurrent programs
- weak/relaxed memory models
- interactive theorem proving in Coq
- compiler verification
INTERNS: A few summer internships (3- or 4-month) are available for
highly qualified undergraduate or graduate students as well.
Successful applicants will join the Foundations of Programming group,
led by me at the Max Planck Institute for Software Systems (MPI-SWS),
which is part of the Saarland Informatics Campus 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 (former manager of the Rust team at
Mozilla), Jacques-Henri Jourdan, Ori Lahav, Pierre-Marie Pédrot,
Azalea Raad, and Rodolphe Lepigre. 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, Joshua Yanovski, and Michael Sammler. The RustBelt project
benefits from longstanding active collaborations with Deepak Garg
(MPI-SWS), Viktor Vafeiadis (MPI-SWS), Lars Birkedal (Aarhus
University), Chung-Kil Hur (Seoul National University), Jeehoon Kang
(KAIST), Robbert Krebbers (TU Delft), and Joe Tassarotti (Boston
College), as well as the many contributors to the Iris project
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 my group and want to learn more about the
project, please contact me directly at email@example.com. To apply
for a postdoc (or PhD student or intern) position, please submit a CV
(and/or grade transcript in English), 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.
I am looking forward to receiving your applications!