<div dir="ltr"><div class="gmail_quote gmail_quote_container"><div dir="ltr" class="gmail_attr">I am pleased to announce the availability of a postdoc position in my research group (Foundations of Programming) at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany.</div><div dir="ltr"><div dir="ltr"><div><div><div class="gmail_quote"><div dir="ltr"><br>The group's research is centered mainly around building logical and semantic foundations for interesting programming languages, with a particular focus on Iris, Rust, Rocq, OCaml, and related formal semantics and verification tools (RefinedC, RefinedRust, Verus, DimSum, Quiver, and more).<div><br></div><div>We maintain active collaborations with multiple research groups at MPI-SWS, including those of Deepak Garg, Viktor Vafeiadis, Björn Brandenburg, and Andrea Lattuada.</div><div><br></div><div><b>Postdoc position</b>: I am seeking exceptional postdoc candidates with a strong, internationally competitive track record of research in programming languages and/or verification.  Successful candidates would have the ability to pursue an independent research agenda that fits well with the topics studied in our research group, as well as the opportunity to co-supervise students in the group on a number of different research projects.</div><div><br></div><div>Current and former postdocs in the group include: Aïna Linn Georges, Youngju Song, Emanuele D'Osualdo, Rodolphe Lepigre, Azalea Raad, Pierre-Marie Pédrot, Ori Lahav, Jacques-Henri Jourdan, Aaron Turon, Neel Krishnaswami, Chung-Kil Hur, and Andreas Rossberg.</div><div><br></div><div>General areas of interest to the group include but are not limited to:</div><div><br></div><div>- separation logic / Iris</div><div>- Rust design and verification (RefinedRust, Verus)<br>- substructural/ownership type systems</div><div>- OCaml extensions (e.g. modal types, DRFCaml)</div><div>- systems verification (RefinedC, Islaris)</div><div>- concurrent program verification</div><div>- probabilistic program verification</div><div>- incorrectness logic / outcome logic</div><div>- effect systems<br>- weak/relaxed memory models<br>- interactive theorem proving in Rocq<br>- compiler verification / secure compilation<br><br>The working language at MPI-SWS is English.  The position is for 2 years, with a possible extension.</div><div><br></div><div>If you are interested in joining my group and want to learn more about the position, please contact me directly at <a href="mailto:dreyer@mpi-sws.org" target="_blank">dreyer@mpi-sws.org</a>.  To apply for a postdoc position, please submit a CV, research statement, and list of references to <a href="https://urldefense.com/v3/__https://apply.cis.mpg.de__;!!IBzWLUs!X2k-XfGB6_9G7X5A7JyRydBIYbrnws6Wx-rtk5rkENj5n4IoagnZ8CeYNzmhcD1-p3ZvIchBtirX-fwq7eHeG2FUBwBU0iA$" target="_blank">https://apply.cis.mpg.de</a> and let me know that you have done so.</div><div><br></div><div><b>Deadline: March 15.</b></div><div><br></div><div>I am looking forward to receiving your applications!<br><br>Best regards,<br>Derek Dreyer</div><div>Scientific Director, MPI-SWS</div><div><br></div></div>
</div></div></div></div>
</div>
</div></div>