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 :
Theses
Complete list of metadatas

Cited literature [89 references]  Display  Hide  Download

https://hal.inria.fr/tel-01086106
Contributor : Jonathan Protzenko <>
Submitted on : Saturday, November 22, 2014 - 2:35:08 AM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Friday, April 14, 2017 - 7:06:47 PM

Licence


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

Identifiers

  • HAL Id : tel-01086106, version 1

Collections

Citation

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

Share

Metrics

Record views

314

Files downloads

448