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 metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01081194
Contributor : François Pottier <>
Submitted on : Friday, November 7, 2014 - 11:46:32 AM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Friday, April 14, 2017 - 11:36:54 AM

File

bpp-mezzo.pdf
Files produced by the author(s)

Identifiers

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

Share

Metrics

Record views

271

Files downloads

189