The Design and Formalization of Mezzo, a Permission-Based Programming Language - Archive ouverte HAL Access content directly
Journal Articles ACM Transactions on Programming Languages and Systems (TOPLAS) Year : 2016

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

(1, 2) , (3) , (3)
1
2
3

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.
Fichier principal
Vignette du fichier
bpp-mezzo-journal.pdf (1022.32 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01246534 , version 1 (18-12-2015)

Identifiers

Cite

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), 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩. ⟨hal-01246534⟩
229 View
258 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More