Auteur : Jules Villard (LSV - ENS Cachan) Titre : Proving Copyless Message Passing Abstract : Handling concurrency using a shared memory and locks can be tedious and error-prone. One solution is to use message-passing instead. We study here a particular flavor that makes the ownership transfer of messages explicit. In this case, ownership of the heap region representing the content of a message is lost upon sending, which can lead to efficient implementations. We have defined a proof system for a concurrent imperative programming language implementing this idea and inspired by the Singularity operating system research project. The proof system, which we have proved sound, is an extension of separation logic, a logic that has already been used successfully to study various ownership-oriented paradigms. In this talk, I will present the programming language, the properties we can prove using our logic, and give some insights about the semantics of our objects. This is joint work with Etienne Lozes (LSV) and Cristiano Calcagno (Imperial College).