Vendredi 6 Décembre

Retour à la vue des calendrier
Vendredi 6 Décembre
Heure: 00:59 - 11:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Data-race freedom by typing in Mezzo
Description: Thibaut Balabonski Mezzo is a typed programming language in the ML family whose static discipline controls aliasing and ownership. This rules out certain mistakes, including representation exposure and data races, and opens up new opportunities, such as gradual initialization or (more generally, and somewhat speculatively) the definition and enforcement of object protocols.

In this talk, I will explain the basic design of Mezzo on examples, and show how its type system inspired by separation logic gives a simple way of tracking ownership of fragments of shared memory between concurrent threads. Beyond the usual claim that "well-typed programs do not go wrong", we guarantee that well-typed Mezzo programs have no data-races.