Ownership Types in Rust

Welcome back to Papers We Love, Zurich!

In this session, Daniel Galán Pascual, a PhD student in the Information Security group at ETH Zürich, will present "A Gentle Introduction to Ownership Types in Rust". Ownership types are what give Rust its memory safety guarantees: the compiler statically rules out entire classes of bugs (use-after-free, data races, dangling pointers) with no garbage collector and no runtime cost. Through worked examples, the talk builds a working understanding of ownership in practice, drawing on the conceptual model of "A Grounded Conceptual Model for Ownership Types in Rust" and its accompanying Aquascope tool.

Why care?

• For systems programmers: ownership types are a general approach to resource management that shows up across many languages, with Rust being the most prominent industrial example. The intuition you build means finally making sense of borrow checker errors when they matter most, both in Rust and beyond it.
• For PL and type-theory enthusiasts: ownership types have deep connections to linear and affine type theory. Seeing them in an industrial language reveals how theory meets real-world complexity.

The talk will be 45-60 minutes, followed by discussion, Q&A and snacks.
No prior background in type systems or Rust is required. However, basic systems programming background will be beneficial.