What is Mezzo?
(Description shamelessly stolen from a paper abstract).
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.
More information about Mezzo
Mezzo is designed by François Pottier and Jonathan Protzenko. The language has been formalized using the Coq proof assistant. 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.
We currently have two papers that are relevant to the current state of the Mezzo project. The first one is about the Coq formalization, and the second one is about the language from a more general perspective.
- François Pottier. Type soundness for Core Mezzo. Unpublished, January 2013. [ bib | PDF | abstract ]
- François Pottier and Jonathan Protzenko. Programming with permissions in Mezzo. Submitted, March 2013. [ bib | abstract | PDF ]
We have a blog at Gallium, and there are a few blog posts there about the Mezzo programming language.
- Jonathan Protzenko. An introduction to Mezzo. [ HTML ]
- Jonathan Protzenko. An introduction to Mezzo, continued. [ HTML ]
The talks feature some detailed examples which are type-checked step-by-step, listing the set of available permissions at each step.
- Jonathan Protzenko. An introduction to Mezzo (short). ML Workshop, Sep 2012. [ PDF | YouTube ]
- Jonathan Protzenko. An introduction to Mezzo [ PDF ]
- The latest version of the Coq proof.
- The latest snapshot of the prototype source code. Requires OCaml 4.00+, as well as the following tools/libraries: Menhir, MenhirLib, Yojson, Ulex, PPrint. Has been tested on Unix environments only. We recommend OPAM to easily install all the dependencies as well as a recent OCaml compiler.
- Generated documentation for the prototype's source code, including the scary dependency graph between modules. The documentation is fairly incomplete, since most .mli files are missing, but the source code does have comments.
- Latest git source. Please contact us if you're interested.
We showcase here some programs written using Mezzo. More code samples are available in the prototype's source code, in the corelib, stdlib and tests directories.
listmodule (implementation, interface) provides operations on lists.
bucketmodule (implementation, interface) provides mutable lists of key-value pairs. It is used mainly by the
hashtablemodule (implementation, interface) defines hash tables.
mutableTreeMapmodule (implementation, interface) defines mutable tree maps using inspiration from the OCaml
queuemodule (implementation, interface) defines a FIFO queue using adoption/abandon. It's an extended version of the module shown in papers and during talks.
vectormodule (implementation, interface) provides resizable arrays.
lazymodule (implementation, interface) provides a way to deal with thunks, i.e. suspensions.
memoizemodule (implementation, interface). provides a library for memoizing the calls to a function using a hashtable internally.
persistentarraymodule (implementation, interface).
bfsmodule (implementation, interface) provides a generic interface for breadth-first traversal of graphs.
dfsmodule (implementation, interface).
nestmodule (interface) axiomatizes Boyland's nesting.
lockmodule (interface) shows our axiomatization of classical locks.
wrefmodule (implementation, interface) shows how to obtain “weak” references (ML-style) by using a lock to protect the invariant.
Graphical error messages with graphs
The type-checker has a feature where it can dump a graphical representation of its state to help understand a type error, or understand how a merge conflict was resolved. We provide a gallery of such dumps. Warning: works only on recent Firefox versions (I'm using ECMAScript 6 features).