Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : François Pottier Connect in order to contact the contributor
Submitted on : Friday, November 7, 2014 - 11:46:32 AM
Last modification on : Friday, January 21, 2022 - 3:14:14 AM
Long-term archiving on: : Friday, April 14, 2017 - 11:36:54 AM


Files produced by the author(s)




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. pp.253 - 269, ⟨10.1007/978-3-319-07151-0_16⟩. ⟨hal-01081194⟩



Les métriques sont temporairement indisponibles