License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.365
URN: urn:nbn:de:0030-drops-52080
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5208/
Go to the corresponding LIPIcs Volume Portal

Vergu, Vlad ; Neron, Pierre ; Visser, Eelco

DynSem: A DSL for Dynamic Semantics Specification

pdf-format:
28.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{vergu_et_al:LIPIcs:2015:5208,
  author =	{Vlad Vergu and Pierre Neron and Eelco Visser},
  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 =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5208},
  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}
}

Keywords: programming languages, dynamic semantics, reduction semantics, semantics engineering, IDE, interpreters, modularity
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

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