Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 18 décembre, 10h30

                            ---------------------
                            Jacques-Henri Jourdan
                            ---------------------

                                     CNRS

     ===================================================================
     RustBelt: Securing the Foundations of the Rust Programming Language
     ===================================================================

Rust is a new language developed at Mozilla Research that marries
together the low-level flexibility of modern C++ with a strong
"ownership-based" type system guaranteeing type safety, memory safety,
and data race freedom. Unfortunately, none of Rust's safety claims have
been formally investigated, and it is not at all clear that they hold.
An important challenge in such a proof resides in the "extensible"
nature of the type system: it is common, in Rust, to extend the
expressive power of the language through libraries that internally use
unsafe features while still being encapsulated in a safe interface.

In this talk, after giving a brief tutorial of the Rust programming
language, I will present RustBelt, our formalization of a realistic
subset of Rust's type system. The formalization starts by defining
LambdaRust, our idealization of Rust's Mid-level Intermediate
Representation (MIR) and giving it a type system. Then, we use
separation logic in order to give a semantic model for types as a
logical relation. This steps requires the formalization of our "lifetime
logic" in order to give a model to the notion of borrows and lifetimes,
which are pervasive in the type system. Finally, we demonstrate the
extensible nature of our proof by modeling some of the most important
types provided by the standard library that significantly extend the
expressive power of the language by safely encapsulating unsafe code.