The Design and Formalization of Mezzo, a Permission-Based Programming Language

Abstract : The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We give a comprehensive tutorial overview of the language. Then, we present a modular formalization of Mezzo's core type system, in the form of a concurrent λ-calculus, which we successively extend with references, locks, and adoption and abandon, a novel mechanism that marries Mezzo's static ownership discipline with dynamic ownership tests. We prove that well-typed programs do not go wrong and are data-race free. Our definitions and proofs are machine-checked.
Type de document :
Article dans une revue
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2016, 38 (4), pp.94. <10.1145/2837022>
Liste complète des métadonnées


https://hal.inria.fr/hal-01246534
Contributeur : François Pottier <>
Soumis le : vendredi 18 décembre 2015 - 16:34:18
Dernière modification le : samedi 18 février 2017 - 01:10:21
Document(s) archivé(s) le : samedi 29 avril 2017 - 22:13:17

Fichier

bpp-mezzo-journal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Thibaut Balabonski, François Pottier, Jonathan Protzenko. The Design and Formalization of Mezzo, a Permission-Based Programming Language. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2016, 38 (4), pp.94. <10.1145/2837022>. <hal-01246534>

Partager

Métriques

Consultations de
la notice

354

Téléchargements du document

85