I am assistant professor at ETH Zürich as part of the Institute for Programming Languages and Systems. Previously, I completed my PhD at MPI-SWS and Saarland University in Saarbrücken, Germany; my advisor was Derek Dreyer. I also did a post-doc in the PDOS group at MIT CSAIL.
I am offering up to two fully funded PhD positions in my newly founded research group at ETH Zürich, with flexible start date. I am looking for strong students that want to do research at the foundations of programming language theory, in program verification and separation logic, with a focus on Rust and Iris. Knowledge of Coq is greatly appreciated. Interested candidates can contact me directly. Please explain why you are interested in a PhD in this field and what your prior experience is. Also include a CV and possible contacts for recommendation letters.
My two main lines of work are about Rust and Iris.
On the Rust side, I am working (also in collaboration with the Rust language team) towards a solid formal foundation for the language, including in particular the unsafe parts.
One key result here is our type safety proof, which also describes a methodology for establishing type safety of well-encapsulated unsafe code.
My goal is to make unsafe Rust just as safe as safe Rust by means of formal verification.
On the Iris side, besides continuing development of its logical foundations, I am interested in applying Iris to new problem domains; recently I started working on modular verification of fault-tolerant distributed system components.
For some more information, check out my research blog, my CV, and my research statement.
In my free time, I like to run internet services myself and work on free software. This goes hand-in-hand with my pursuit of defending our privacy rights and our freedom in the digital world. See my personal website for more information.