Programming with Permissions in Mezzo

Abstract

We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and ownership. This rules out certain mistakes, including representation exposure and data races, and enables new idioms, such as gradual initialization, memory re-use, and (type)state changes. Although the core static discipline disallows sharing a mutable data structure, Mezzo offers several ways of working around this restriction, including a novel dynamic ownership control mechanism which we dub "adoption and abandon".

Cited by in corpus (6)

• Aeneas: Rust Verification by Functional Translation
• Oxide: The Essence of Rust
• Linearly Qualified Types: Generic inference for capabilities and uniqueness
• Object Capabilities and Lightweight Affinity in Scala: Implementation, Formalization, and Soundness
• Resource Polymorphism
• Predicate Abstraction for Linked Data Structures