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. http://plv.mpi-sws.org/rustbelt 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 at http://iris-project.org/). 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 topics: - 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 dreyer@mpi-sws.org. To apply for a postdoc position, please submit a CV, research statement, and list of references to https://apply.mpi-sws.org. For further information, see the project web page at: http://plv.mpi-sws.org/rustbelt/
Master of Science in Informatics at Grenoble (MOSIG 2016-2020)
