License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.EVCS.2023.29
URN: urn:nbn:de:0030-drops-177991
Go to the corresponding OASIcs Volume Portal

van der Storm, Tijs

Semantics Engineering with Concrete Syntax

OASIcs-EVCS-2023-29.pdf (1 MB)


Semantics engineering tools like Redex can be used to define, explore, and debug formal definitions of programming language semantics. However, such tools are often based on abstract syntax, which makes the definition of rules and the exploration of execution traces rather unfriendly. In this paper we introduce Credex, a library in the Rascal meta-programming language for defining small-step evaluation-context semantics, where terms and matching patterns are what-you-see-is-what-you-get. Credex employs parsing for decomposing terms into context and redex. Since Rascal’s grammar formalism is based on general parsing, a non-unique decomposition of a term literally corresponds to an ambiguous parse. We demonstrate the use of Credex, detail some aspects of its implementation, and discuss three case-studies.

BibTeX - Entry

  author =	{van der Storm, Tijs},
  title =	{{Semantics Engineering with Concrete Syntax}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{29:1--29:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-177991},
  doi =		{10.4230/OASIcs.EVCS.2023.29},
  annote =	{Keywords: Semantics engineering, syntax, parsing, reduction semantics}

Keywords: Semantics engineering, syntax, parsing, reduction semantics
Collection: Eelco Visser Commemorative Symposium (EVCS 2023)
Issue Date: 2023
Date of publication: 21.03.2023

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