Mezzo: a typed language for safe effectful concurrent programs - Archive ouverte HAL Access content directly
Theses Year : 2014

Mezzo: a typed language for safe effectful concurrent programs

Mezzo: un langage typé pour programmer de manière concurrent et sure en présence d'effets

(1)
1

Abstract

The present dissertation argues that better programming languages can be designed and implemented, so as to provide greater safety and reliability for computer programs. I sustain my claims through the example of Mezzo, a programming language in the tradition of ML, which I co-designed and implemented. Programs written in Mezzo enjoy stronger properties than programs written in traditional ML languages: they are data-race free; state changes can be tracked by the type system; a central notion of ownership facilitates modular reasoning. Mezzo is not the first attempt at designing a better programming language; hence, a first part strives to position Mezzo relative to other works in the literature. I present landmark results in the field, which served either as sources of inspiration or points of comparison. The subse- quent part is about the design of the Mezzo language. Using a variety of examples, I illustrate the language features as well as the safety gains that one obtains by writing their programs in Mezzo. In a subsequent part, I formalize the semantics of the Mezzo language. Mezzo is not just a type system that lives on paper: the final part describes the implementation of a type-checker for Mezzo, by formalizing the algorithms that I designed and the various ways the type-checker ensures that a program is valid.
Cette thèse décrit comment obtenir de plus fortes garanties de sûreté pour les programmes en utilisant Mezzo, un langage de programmation inspiré par ML, et muni d’un système de types novateur. Les programmes écrits en Mezzo bénéficient de plus fortes garanties, com- parés à des programmes équivalents écrits dans un dialecte de ML: absence de séquencements critiques (« race conditions »), suivi des changements d’états au travers du système de types, et une notion de possession qui facilite le raisonnement modulaire et la compréhension des programmes.Mezzo n’est pas la premier langage à s’attaquer à cet objectif louable : une première partie s’efforce donc de situer Mezzo dans son contexte, en présentant des travaux emblématiques de la recherche en langages de programmation, travaux qui ont constitué des sources d’inspiration ou ont servi de points de comparaison. Une seconde partie présente le langage. Tout d’abord, au travers d’une riche palette d’exemples, qui permettent d’illustrer les fonctionnalités du lan- gage ainsi que les gains de sûreté qui en découlent. Puis, dans une partie suivante, de manière formelle, en détaillant les différentes règles qui gouvernent le système de types de Mezzo. Mezzo n’existe pas seulement sur le papier : une dernière partie décrit la manière dont le lan- gage est implémenté, en formalisant les algorithmes utilisés dans le typeur et en détaillant les techniques utilisées pour déterminer la validité d’un programme.
Fichier principal
Vignette du fichier
snapshot-0909.pdf (1.24 Mo) Télécharger le fichier
Loading...

Dates and versions

tel-01086106 , version 1 (22-11-2014)

Licence

Attribution - NonCommercial - ShareAlike - CC BY 4.0

Identifiers

  • HAL Id : tel-01086106 , version 1

Cite

Jonathan Protzenko. Mezzo: a typed language for safe effectful concurrent programs. Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2014. English. ⟨NNT : ⟩. ⟨tel-01086106⟩

Collections

INRIA INRIA2
179 View
368 Download

Share

Gmail Facebook Twitter LinkedIn More