Type Soundness and Race Freedom for Mezzo

Abstract : The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We incorporate shared-memory concurrency into Mezzo and present a mod-ular formalization of its core type system, in the form of a concurrent λ-calculus, which we extend with references and locks. We prove that well-typed programs do not go wrong and are data-race free. Our definitions and proofs are machine-checked.
Type de document :
Communication dans un congrès
FLOPS 2014: 12th International Symposium on Functional and Logic Programming, Jun 2014, Kanazawa, Japan. Springer, 8475, pp.253 - 269, 2014, LNCS. <10.1007/978-3-319-07151-0_16>
Liste complète des métadonnées

https://hal.inria.fr/hal-01081194
Contributeur : François Pottier <>
Soumis le : vendredi 7 novembre 2014 - 11:46:32
Dernière modification le : lundi 5 octobre 2015 - 17:00:55

Fichier

bpp-mezzo.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Thibaut Balabonski, François Pottier, Jonathan Protzenko. Type Soundness and Race Freedom for Mezzo. FLOPS 2014: 12th International Symposium on Functional and Logic Programming, Jun 2014, Kanazawa, Japan. Springer, 8475, pp.253 - 269, 2014, LNCS. <10.1007/978-3-319-07151-0_16>. <hal-01081194>

Partager

Métriques

Consultations de
la notice

123

Téléchargements du document

113