The Mezzo programming language

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 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.

Mezzo on the web!

Run Mezzo in your browser!

Learn interactively how Mezzo programs are type-checked: first example, second example.

See how Mezzo solves a complex type-checking situation (requires Firefox).

Read the unfinished, boring tutorial!

Some reading

Papers

Several papers about Mezzo appeared over the course of the past few years. The paragraph below lists them all; however, only two of these are relevant at the time of this writing.

The currently-submitted journal paper contains: an exhaustive tutorial about the language; a formal description of “Simple Mezzo”, a restricted subset of Mezzo, along with corresponding typing rules; the description of our Coq formalization of Simple Mezzo. This paper subsumes the ICFP'13 and FLOPS'14 papers.

The PhD dissertation contains, among other things: an extended version of the tutorial; the formalization of the “is duplicable” and “is exclusive” predicates; a complete description of the implementation of the Mezzo type-checker. This subsumes the IFL'13 paper (not listed here).

• Jonathan Protzenko. Mezzo, the language of the future. PhD Dissertation (current status: pending final review). [ PDF ]
• Thibaut Balabonski, François Pottier, and Jonathan Protzenko. The design and formalization of Mezzo, a permission-based programming language. Submitted for publication, July 2014. [ bib | PDF | Abstract ]
• Thibaut Balabonski, François Pottier, and Jonathan Protzenko. Type soundness and race freedom for Mezzo. FLOPS'14. [ bib | PDF | abstract ]
• Armaël Guéneau, François Pottier, and Jonathan Protzenko. The ins and outs of iteration in Mezzo. HOPE'13. [ bib | PDF ]
• François Pottier and Jonathan Protzenko. Programming with permissions in Mezzo. ICFP'13. Long version updated May 2013. [ bib | abstract | PDF | PDF (long) ]
• François Pottier and Jonathan Protzenko. Programming with permissions: the Mezzo language (extended abstract). ML Workshop, Sep 2012. [ PDF ]

Blog posts

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 ]

Talks

The talks feature some detailed examples which are type-checked step-by-step, listing the set of available permissions at each step.

• Jonathan Protzenko. The implementation of Mezzo. IFL'13. [ PDF ]
• Jonathan Protzenko. Why design a new programming language?. FSFMA'13. [ PDF ]
• Jonathan Protzenko. An introduction to Mezzo (short). ML Workshop, Sep 2012. [ PDF | YouTube ]
• Jonathan Protzenko. An introduction to Mezzo [ PDF ]

Downloads

• Mezzo is in OPAM: just hit opam install mezzo
• The older formalisation covers a lot of ground, but is less modular.
• The newer formalisation covers less ground, but is cleaner.
• 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.

Demos

Sample programs

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.

• The list module (implementation, interface) provides operations on lists.
• The bucket module (implementation, interface) provides mutable lists of key-value pairs. It is used mainly by the hashtable module.
• The hashtable module (implementation, interface) defines hash tables.
• The mutableTreeMap module (implementation, interface) defines mutable tree maps using inspiration from the OCaml Map module.
• The queue module (implementation, interface) defines a FIFO queue using adoption/abandon. It's an extended version of the module shown in papers and during talks.
• The vector module (implementation, interface) provides resizable arrays.
• The lazy module (implementation, interface) provides a way to deal with thunks, i.e. suspensions.
• The memoize module (implementation, interface). provides a library for memoizing the calls to a function using a hashtable internally.
• The persistentarray module (implementation, interface).
• The bfs module (implementation, interface) provides a generic interface for breadth-first traversal of graphs.
• The dfs module (implementation, interface).
• The nest module (interface) axiomatizes Boyland's nesting.
• The lock module (interface) shows our axiomatization of classical locks.
• The wref module (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).