2026-07-25T01:47:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4090 2024-03-06T10:29:15Z ddc:004 open_access

Illustrating the Mezzo programming language Protzenko, Jonathan Type system Language design ML Permissions 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jonathan Protzenko 2013 Is Part Of OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FSFMA.2013.68 urn:nbn:de:0030-drops-40905 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.68 eng https://creativecommons.org/licenses/by/3.0/legalcode