DARTS.2.1.10.pdf
- Filesize: 462 kB
- 3 pages
Document
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)
Volume: DARTS, Volume 2 (ECOOP 2016)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Germany license
- Publication Date: 2016-07-14
Artifact Description
Document Identifiers
Cite As Get BibTex
Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser. Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/DARTS.2.1.10
Artifact
DARTS-2-1-10-artifact-41cd2fd85e8469a2ab693515fe291955.zip
(Filesize: 0.57 MB)
MD5 Sum:
41cd2fd85e8469a2ab693515fe291955
(Get MD5 Sum)
Abstract
Our paper introduces a systematic approach to the alignment of names in the static structure of a program, and memory layout and access during its execution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection. This Coq artifact showcases how our uniform model for memory layout in dynamic semantics provides structure to type soundness proofs. The artifact contains type soundness proofs mechanized in Coq for (supersets of) all languages in the paper. The type soundness proofs rely on a language-independent framework formalizing scope graphs and frame heaps.
Subject Classification
Keywords
- Dynamic semantics
- scope graphs
- memory layout
- type soundness
- operational semantics
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In Jan Vitek, editor, ESOP'15, volume 9032 of LNCS, pages 205-231. Springer, 2015.
- Casper Bach Poulsen, Pierre Néron, Andrew P. Tolmach, and Eelco Visser. Scopes describe frames: A uniform model for memory layout in dynamic semantics. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th European Conference on Object-Oriented Programming (ECOOP 2016), volume 56 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:25, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2016.20.
-
Casper Bach Poulsen, Pierre Néron, Andrew P. Tolmach, and Eelco Visser. Scopes describe frames: A uniform model for memory layout in dynamic semantics. Technical Report TUD-SERG-2016-010, Delft University of Technology, Programming Languages Research Group, Delft, The Netherlands, 2016.
-
Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A constraint language for static semantic analysis based on scope graphs. In Martin Erwig and Tiark Rompf, editors, PEPM'16, pages 49-60. ACM, 2016.