Search Results

Documents authored by Néron, Pierre

Document
DOI: 10.4230/LIPIcs.ECOOP.2016.20
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics

Authors: Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Semantic specifications do not make a systematic connection between the names and scopes in the static structure of a program and memory layout, and access during its execution. In this paper, we introduce a systematic approach to the alignment of names in static semantics and memory in dynamic semantics, building on the scope graph framework for name resolution. 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.
Cite as

Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser. Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 20:1-20:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bachpoulsen_et_al:LIPIcs.ECOOP.2016.20,
  author =	{Bach Poulsen, Casper and N\'{e}ron, Pierre and Tolmach, Andrew and Visser, Eelco},
  title =	{{Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{20:1--20:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.20},
  URN =		{urn:nbn:de:0030-drops-61140},
  doi =		{10.4230/LIPIcs.ECOOP.2016.20},
  annote =	{Keywords: Dynamic semantics, scope graphs, memory layout, type soundness, operational semantics}
}
Document
DOI: 10.4230/DARTS.2.1.10
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)

Authors: Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser

Published in: DARTS, Volume 2, Issue 1, Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)

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.
Cite as

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)

Copy BibTex To Clipboard

@Article{bachpoulsen_et_al:DARTS.2.1.10,
  author =	{Bach Poulsen, Casper and Néron, Pierre and Tolmach, Andrew and Visser, Eelco},
  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},
  editor =	{Bach Poulsen, Casper and Néron, Pierre and Tolmach, Andrew and Visser, Eelco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.10},
  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}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.365
DynSem: A DSL for Dynamic Semantics Specification

Authors: Vlad Vergu, Pierre Neron, and Eelco Visser

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
The formal semantics of a programming language and its implementation are typically separately defined, with the risk of divergence such that properties of the formal semantics are not properties of the implementation. In this paper, we present DynSem, a domain-specific language for the specification of the dynamic semantics of programming languages that aims at supporting both formal reasoning and efficient interpretation. DynSem supports the specification of the operational semantics of a language by means of statically typed conditional term reduction rules. DynSem supports concise specification of reduction rules by providing implicit build and match coercions based on reduction arrows and implicit term constructors. DynSem supports modular specification by adopting implicit propagation of semantic components from I-MSOS, which allows omitting propagation of components such as environments and stores from rules that do not affect those. DynSem supports the declaration of native operators for delegation of aspects of the semantics to an external definition or implementation. DynSem supports the definition of auxiliary meta-functions, which can be expressed using regular reduction rules and are subject to semantic component propagation. DynSem specifications are executable through automatic generation of a Java-based AST interpreter.
Cite as

Vlad Vergu, Pierre Neron, and Eelco Visser. DynSem: A DSL for Dynamic Semantics Specification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 365-378, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{vergu_et_al:LIPIcs.RTA.2015.365,
  author =	{Vergu, Vlad and Neron, Pierre and Visser, Eelco},
  title =	{{DynSem: A DSL for Dynamic Semantics Specification}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{365--378},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.365},
  URN =		{urn:nbn:de:0030-drops-52080},
  doi =		{10.4230/LIPIcs.RTA.2015.365},
  annote =	{Keywords: programming languages, dynamic semantics, reduction semantics, semantics engineering, IDE, interpreters, modularity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact