The Design and Formalization of Mezzo, a Permission-Based Programming Language
| Autor: | Thibaut Balabonski, Jonathan Protzenko, François Pottier |
|---|---|
| Přispěvatelé: | Université Paris-Sud - Paris 11 (UP11), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Langages de programmation, types, compilation et preuves (GALLIUM), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
business.industry Programming language Computer science Concurrency Static type systems Ownership 020207 software engineering 0102 computer and information sciences 02 engineering and technology Permission Modular design Mathematical proof computer.software_genre 01 natural sciences Operational semantics 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Polymorphism business Side effects computer Software |
| Zdroj: | ACM Transactions on Programming Languages and Systems (TOPLAS) ACM Transactions on Programming Languages and Systems (TOPLAS), 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩ ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩ |
| ISSN: | 0164-0925 1558-4593 |
| Popis: | International audience; 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 λ-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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|