License: Creative Commons Attribution 3.0 Germany license (CC BY 3.0 DE)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.2.1.10
URN: urn:nbn:de:0030-drops-61314
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6131/
Go back to Dagstuhl Artifacts Series

Bach Poulsen, Casper ; Néron, Pierre ; Tolmach, Andrew ; Visser, Eelco

Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)

pdf-format:
DARTS-2-1-10.pdf (0.5 MB)

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.

BibTeX - Entry

@Article{bachpoulsen_et_al:DARTS:2016:6131,
  author =	{Casper Bach Poulsen and Pierre Néron and Andrew Tolmach and Eelco Visser},
  title =	{{Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)}},
  pages =	{10:1--10:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6131},
  URN =		{urn:nbn:de:0030-drops-61314},
  doi =		{10.4230/DARTS.2.1.10},
  annote =	{Keywords: Dynamic semantics, scope graphs, memory layout, type soundness, operational semantics}
}

Keywords: Dynamic semantics, scope graphs, memory layout, type soundness, operational semantics
Collection: DARTS, Volume 2, Issue 1
Related Scholarly Article: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2016.20
Issue Date: 2016
Date of publication: 14.07.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI