Mezzo: a typed language for safe effectful concurrent programs

Résumé : 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.
Type de document :
Thèse
Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2014. English
Liste complète des métadonnées


https://hal.inria.fr/tel-01086106
Contributeur : Jonathan Protzenko <>
Soumis le : samedi 22 novembre 2014 - 02:35:08
Dernière modification le : lundi 5 octobre 2015 - 16:56:22
Document(s) archivé(s) le : vendredi 14 avril 2017 - 19:06:47

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale - Partage selon les Conditions Initiales 4.0 International License

Identifiants

  • HAL Id : tel-01086106, version 1

Collections

Citation

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

Partager

Métriques

Consultations de
la notice

199

Téléchargements du document

292