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

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01081194
Contributeur : François Pottier <>
Soumis le : vendredi 7 novembre 2014 - 11:46:32
Dernière modification le : mercredi 29 novembre 2017 - 15:14:26
Document(s) archivé(s) le : vendredi 14 avril 2017 - 11:36:54

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

203

Téléchargements de fichiers

118