Illustrating the Mezzo programming language

Abstract : 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.
Type de document :
Pré-publication, Document de travail
2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00910402
Contributeur : Jonathan Protzenko <>
Soumis le : jeudi 28 novembre 2013 - 09:05:07
Dernière modification le : mercredi 27 juillet 2016 - 14:48:48

Identifiants

  • HAL Id : hal-00910402, version 1
  • ARXIV : 1311.6929

Collections

Citation

Jonathan Protzenko. Illustrating the Mezzo programming language. 2013. <hal-00910402>

Partager

Métriques

Consultations de la notice

80