License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FSFMA.2013.68
URN: urn:nbn:de:0030-drops-40905
Go to the corresponding OASIcs Volume Portal

Protzenko, Jonathan

Illustrating the Mezzo programming language

10.pdf (0.4 MB)


When programmers want to prove strong program invariants, they are usually faced with a choice between using theorem provers and using traditional programming languages. The former requires them to provide program proofs, which, for many applications, is considered a heavy burden. The latter provides less guarantees and the programmer usually has to write run-time assertions to compensate for the lack of suitable invariants expressible in the type system.

We introduce Mezzo, a programming language in the tradition of ML, in which the usual concept of a type is replaced by a more precise notion of a permission. Programs written in Mezzo usually enjoy stronger guarantees than programs written in pure ML. However, because Mezzo is based on a type system, the reasoning requires no user input. In this paper, we illustrate the key concepts of Mezzo, highlighting the static guarantees our language provides.

BibTeX - Entry

  author =	{Jonathan Protzenko},
  title =	{{Illustrating the Mezzo programming language}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{68--73},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Christine Choppy and Jun Sun},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-40905},
  doi =		{10.4230/OASIcs.FSFMA.2013.68},
  annote =	{Keywords: Type system, Language design, ML, Permissions}

Keywords: Type system, Language design, ML, Permissions
Collection: 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Issue Date: 2013
Date of publication: 14.07.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI