Programming with permissions: the Mezzo language

Jonathan Protzenko (1) , François Pottier (1)

1 GALLIUM - Programming languages, types, compilation and proofs

Mezzo is a functional programming language with effects, in the tradition of ML. Mezzo aims to provide a successor to OCaml with afiner control of aliasing and effects. We offer stronger static guarantees on the mutable store: programs written in Mezzo enjoy non-aliasing and separation properties. This fine-grained control ofownership and effects allows Mezzo to type-check programs previously deemed unsafe by the OCaml type-checker.

Domaines: Langage de programmation [cs.PL]

Jonathan Protzenko, François Pottier. Programming with permissions: the Mezzo language. ACM SIGPLAN Workshop on ML, Sep 2012, Copenhagen, Denmark. ⟨hal-01092204⟩