Sites Inria

English version

Séminaire des équipes de recherche

Formalizing the essence of Rust's type system with the Iris separation logic

© INRIA Sophie Auvin - G comme Grille

  • Date : 9/01/2017
  • Lieu : Inria de Paris, 2 rue Simone Iff, 75012 Paris - Salle Jacques-Louis Lions 1, bâtiment C - 10h30
  • Intervenant(s) : Jacques-Henri Jourdan- MPI-SWS

He Rust programming language, whose first version has been recently released by Mozilla, gives high performance and low-level control over the machine's resources. However, contrary to other systems programming languages such as C or C++, its type system provides
strong safety guarantees. They include memory safety, but also no undesired aliasing and absence of data races. In order to fulfill these two apparently opposed objectives, Rust follows an ownership discipline based on a so-called "borrowing" mechanism.

In this talk, I will give a brief overview of the main features of Rust. I will explain why giving a formal proof of soundness of this type system is an interesting challenge. I will present our ongoing project of formalizing a core fragment using the recently developed Iris concurrent separation logic, of which I will give a brief overview.

Even more challenging, the standard library of Rust contains data structures providing "interior mutability". These data structures allow to mutate aliased pointers while keeping the strong guarantees by following carefully designed rules enforced statically or dynamically.

Mots-clés : India de Paris Formalizing Essence Rust's type system Iris Logic Gallium

Haut de page

Suivez Inria