Skip to Main content Skip to Navigation
Journal articles

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 metadata

Cited literature [105 references]  Display  Hide  Download
Contributor : François Pottier Connect in order to contact the contributor
Submitted on : Friday, December 18, 2015 - 4:34:18 PM
Last modification on : Friday, January 21, 2022 - 3:19:58 AM
Long-term archiving on: : Saturday, April 29, 2017 - 10:13:17 PM


Files produced by the author(s)



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⟩



Les métriques sont temporairement indisponibles