Skip to Main content Skip to Navigation

Mezzo: a typed language for safe effectful concurrent programs

Abstract : The present dissertation argues that better programming languages can be designed and implemented, so as to provide greater safety and reliability for computer programs. I sustain my claims through the example of Mezzo, a programming language in the tradition of ML, which I co-designed and implemented. Programs written in Mezzo enjoy stronger properties than programs written in traditional ML languages: they are data-race free; state changes can be tracked by the type system; a central notion of ownership facilitates modular reasoning. Mezzo is not the first attempt at designing a better programming language; hence, a first part strives to position Mezzo relative to other works in the literature. I present landmark results in the field, which served either as sources of inspiration or points of comparison. The subse- quent part is about the design of the Mezzo language. Using a variety of examples, I illustrate the language features as well as the safety gains that one obtains by writing their programs in Mezzo. In a subsequent part, I formalize the semantics of the Mezzo language. Mezzo is not just a type system that lives on paper: the final part describes the implementation of a type-checker for Mezzo, by formalizing the algorithms that I designed and the various ways the type-checker ensures that a program is valid.
Document type :
Complete list of metadata

Cited literature [89 references]  Display  Hide  Download
Contributor : Jonathan Protzenko Connect in order to contact the contributor
Submitted on : Saturday, November 22, 2014 - 2:35:08 AM
Last modification on : Tuesday, January 11, 2022 - 11:16:26 AM
Long-term archiving on: : Friday, April 14, 2017 - 7:06:47 PM


Distributed under a Creative Commons Attribution - NonCommercial - ShareAlike 4.0 International License


  • HAL Id : tel-01086106, version 1



Jonathan Protzenko. Mezzo: a typed language for safe effectful concurrent programs. Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2014. English. ⟨tel-01086106⟩



Les métriques sont temporairement indisponibles