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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [105 references]  Display  Hide  Download

https://hal.inria.fr/hal-01246534
Contributor : François Pottier <>
Submitted on : Friday, December 18, 2015 - 4:34:18 PM
Last modification on : Thursday, April 26, 2018 - 10:28:14 AM
Long-term archiving on : Saturday, April 29, 2017 - 10:13:17 PM

File

bpp-mezzo-journal.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

520

Files downloads

211