Reminder this is today at 1pm.
Heads up: Ralf Jung (
https://www.ralfj.de/research/) will be giving a talk this Friday at our pl-seminar. He'll talk about his thesis work which won a number of awards.
RustBelt Rust is a young systems programming language that aims to fill the gap between high-level languages — which provide strong static guarantees like memory and thread safety — and low-level languages — which give the programmer fine-grained control over
data layout and memory management. This talk gives an introduction to RustBelt, a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. The model is designed to verify the safety of a number of intricate
APIs from the Rust standard library, despite the fact that the implementations of these APIs use unsafe language features. After explaining the basics of RustBelt and the general approach of semantic type safety, we will look at the safety proof of one particularly
interesting Rust API: the Cell type, which seemingly breaks some of the fundamental constraints of the Rust type system by permitting mutation of shared state.
I am a post-doctoral researcher in the PDOS group at MIT CSAIL under the supervision of Frans Kaashoek and Nickolai Zeldovich. Previously, I completed my PhD at MPI-SWS and Saarland University in Saarbrücken, Germany; my advisor was Derek Dreyer.. I am on the
academic job market this year (fall 2021), mostly looking for faculty positions in Europe.
www.ralfj.de
|