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 modular 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. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Balabonski, T., Pottier, F., & Protzenko, J. (2014). Type soundness and race freedom for Mezzo. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8475 LNCS, pp. 253–269). Springer Verlag. https://doi.org/10.1007/978-3-319-07151-0_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
