The Design and Formalization of Mezzo, a Permission-Based Programming Language
The Design and Formalization of Mezzo, a Permission-Based Programming Language
复制标题
DOI：
10.1145/2837022
复制
发表时间：
2016-10-01
影响因子：
1.3
通讯作者：
Protzenko, Jonathan
中科院分区：
文献类型：
--
作者：
Balabonski, Thibaut;Pottier, Francois;Protzenko, Jonathan
编程语言Mezzo配备了一种丰富的类型系统，该系统控制着混叠和访问可变内存。我们提供了该语言的全面教程概述。然后，我们以并发的lambda-calculus的形式呈现了Mezzo的核心类型系统的模块化形式化，我们将其连续地扩展到参考，锁和采用和放弃，这是一种与动态所有权测试相结合的新型机制，该机制与Mezzo的静态所有权纪律结合。我们证明，良好的程序不会出错，并且没有数据竞赛。我们的定义和证明是机器检查的。
The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We give a comprehensive tutorial overview of the language. Then we present a modular formalization of Mezzo's core type system, in the form of a concurrent lambda-calculus, which we successively extend with references, locks, and adoption and abandon, a novel mechanism that marries Mezzo's static ownership discipline with dynamic ownership tests. We prove that well-typed programs do not go wrong and are data-race free. Our definitions and proofs are machine checked.