<p>My two main lines of work are about <a href="https://www.rust-lang.org/">Rust</a> and <a href="https://iris-project.org/">Iris</a>.<br>
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 <a href="https://plv.mpi-sws.org/rustbelt/popl18/">type safety proof</a>, which also describes a methodology for establishing type safety of well-encapsulated unsafe code.
<p>My two main lines of work are about <a href="https://www.rust-lang.org/">Rust</a> and <a href="https://iris-project.org/">Iris</a>.<br>
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 <a href="https://plv.mpi-sws.org/rustbelt/popl18/">type safety proof</a>, which also describes a methodology for establishing type safety of well-encapsulated unsafe code.