We present the design of Mezzo, a programming language in the ML tradition, which places strong emphasis on the control of aliasing and access to mutable memory. A balance between simplicity and expressiveness is achieved by marrying a static discipline of permissions and a dynamic mechanism of adoption and abandon. Mezzo is designed by François Pottier and Jonathan Protzenko. The language has been formalized using the Coq proof assistant by François Pottier and Thibaut Balabonski. We currently have a prototype implementation of a type-checker. We have several papers, abstracts and presentations that describe the language. Since the language is always in flux, it is best to refer to the most recent publication.
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Charguéraud, Arthur; Pottier, François: Temporary Read-only permissions for separation logic (2017)
- Balabonski, Thibaut; Pottier, François; Protzenko, Jonathan: Type soundness and race freedom for mezzo (2014)
- Pottier, François; Protzenko, Jonathan: Programming with permissions in Mezzo (2013) ioport