Type Soundness and Race Freedom for Mezzo.
Lecture Notes in Computer Science(2014)
摘要
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 lambda-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.
更多查看译文
关键词
Machine State, Operational Semantic, Typing Rule, Type Soundness, Separation Logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要