Standard

Scopes Describe Frames : A Uniform Model for Memory Layout in Dynamic Semantics (Artifact). / Poulsen, Casper Bach ; Neron, Pierre; Tolmach, Andrew; Visser, Eelco.

2016. 1-3 ECOOP 2016, Rome, Italy.

Research output: Contribution to conferenceOtherOther research output

Harvard

APA

Vancouver

Author

BibTeX

@conference{03afebbf31704ecabde9e5a90f0fdcc4,
title = "Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)",
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.",
author = "Poulsen, {Casper Bach} and Pierre Neron and Andrew Tolmach and Eelco Visser",
year = "2016",
doi = "10.4230/DARTS.2.1.10",
language = "English",
pages = "1--3",
note = "ECOOP 2016 : 30th European Conference on Object-Oriented Programming ; Conference date: 18-07-2016 Through 22-07-2016",

}

RIS

TY - CONF

T1 - Scopes Describe Frames

T2 - A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)

AU - Poulsen, Casper Bach

AU - Neron, Pierre

AU - Tolmach, Andrew

AU - Visser, Eelco

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://resolver.tudelft.nl/uuid://03afebbf-3170-4eca-bde9-e5a90f0fdcc4

U2 - 10.4230/DARTS.2.1.10

DO - 10.4230/DARTS.2.1.10

M3 - Other

SP - 1

EP - 3

ER -

ID: 9993614